Lógica temporal linea

Para esta semana en la clase de validación hablamos del tema de la lógica temporal lineal, en la cual se habla sobre operadores lógicos asociados con eventos en tiempo.
 

[Imagen obtenida de:"http://www.moma.org/collection_images/resized/051/w500h420/CRI_151051.jpg"]

Símbolos aprendidos de lógica temporal

Este símbolo representa un evento que en algún momento se cumple.
 

Este símbolo representa un evento que se cumple en el siguiente estado.

Este símbolo representa un evento que en cualquier estado se cumple.

Mi problema
Como tarea se nos encargo resolver un inciso de los problemas del capitulo 14 del siguiente curso del profesor Andrei Voronkov:
http://www.voronkov.com/lics.cgi

El inciso que elegí es el siguiente:
Ejercicio 14.7 inciso (3).
Considerando el sistema de transición con el siguiente grafo de transiciones de estados.

Es verdadero el siguiente enunciado?

Conclusión
El enunciado es verdadero ya que el enunciado denota que existe algún estado para el cuál se cumple el evento y en al menos en el estado inferior derecho "y" cumple que tiene valor uno.

Referencias:
http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14
http://es.wikipedia.org/wiki/L%C3%B3gica_temporal