domingo, 18 de noviembre de 2012

Tarea 12: Computation Tree Logic

Para está entrada mi ejercicio es el siguiente:


La cual trata de convertirla a CTL, en caso de que sea imposible explicar el porque.

Para que sea mas fácil su construcción, primero definiremos su sintaxis... pero antes que nada definamos los operadores:


Resaltando las palabars claves de nuestro enunciado:
p es verdadera en el estado actual y alguna ruta y en algun tiempo futuro tendra q verdadera.
Lo cual se puede interpretar de la siguiente forma:
EU q
entonces su contrucción quedaria(los puntos celestes es donde se cumplen la condiccioón para "p" y los puntos rojos en para "q"):


Representando la misma expresión con la estrucura de Kripke tendremos:

Estrucura general de Kripke

Estructura de Kripke para "p EU q"


Referencias:
http://en.wikipedia.org/wiki/Computation_tree_logic
A good document on Computation Tree Logic.
http://elisa.dyndns-web.com/~elisa/teaching/sys/valid/ctl.pdf