Tarea 11: Linear temporal logic

Mi ejercicio para esta tarea es el siguiente:

Traducido: Ejercicio 14.4: Encontrar dos diferentes fórmulas del ejercicio 14.3 que son equivalentes entre sí.

Las fórmulas del ejercicio 14.3 son las siguientes:

Para poder saber si son iguales o representan lo mismo, me parece mucho más fácil verificarlas pasandolas a un enunciado, en vez de simbolos, haciendo esto quedan aproximadamente de la siguiente manera:

(1 ) En un futuro siempre A.
(2 ) Siempre(Si A es el estado actual, entonces A es el siguiente estado)
(3 ) No A hasta que siempre A.
(4 ) A hasta que no A.
(5 ) En un Futuro A y Siempre(A si A es el siguiente estado)

Viendolo de esta manera, las expresiones (1) y (5) claramente suenan equivalentes, y todas significan lo mismo, que puede expresarse algo así.

  ---->o---->o---->A---->A---->A---->A

1. En un futuro, siempre A. En un futuro siempre se estará en el estado A.
5. En un Futuro A ^ Siempre A sí A es el siguiente estado. En un futuro se estará en el estado A y siempre si el estado A es el actual, A es el siguiente.