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:
Representando la misma expresión con la estrucura de Kripke tendremos:
Referencias:
http://en.wikipedia.org/wiki/Computation_tree_logic
A good document on Computation Tree Logic.
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:
p EU qentonces 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.
La E y la U no realmente se pueden combinar de esa manera; podría ser algo como E(x U y) y lo de futuro saldría más natural con lo de F que con U La gráfica del arbolito sí tiene algo de sentido. Yo iría por p ^ EFq. Van 4 pts por el intento.
ResponderEliminar