Tarea 12 - CTL

Introducción

Computación árbol lógico (CTL) es una derivación lógica de tiempo, lo que significa que su modelo de tiempo es una estructura en forma de árbol en la que el futuro no está determinado, hay diferentes caminos en el futuro, cualquiera de las cuales podría ser un camino real que se realiza. Se utiliza en la verificación formal de artefactos de software o hardware, típicamente por aplicaciones de software conocidas como fichas del modelo que determinan si un artefacto dado posee seguridad o propiedades de vida de la conexión. Por ejemplo, CTL puede especificar que cuando alguna condición inicial es satisfecha (por ejemplo, todas las variables de programa son los coches positivos o no en un straddle carretera de dos carriles), entonces todas las ejecuciones posibles de un programa evitar una condición indeseable (por ejemplo, la división de un número por cero o dos coches chocan en una autopista). En este ejemplo, la propiedad de seguridad podría ser verificado por un verificador de modelo que explora todas las posibles transiciones de estados del programa que satisfacen la condición inicial y asegura que todas las ejecuciones éstos se ajustan a la propiedad. Lógica Computación árbol pertenece a una clase de lógicas temporales que incluyen la lógica lineal temporal (LTL). Aunque hay propiedades expresable en sólo uno de CTL y LTL, todas las propiedades expresables en cualquiera de lógica también se puede expresar en * CTL.

Problema

2.14. Along all paths, p alternates between being true and being false in each successive state

Lo significa: 

2.14. A lo largo de todos los caminos, p alterna entre ser verdadero o ser falso en cada estado sucesivo.


Respuesta

Vamos a usar estos operadores:

A =∀ = Siempre
U = Hasta
X = o = Siguiente

Bibliografía

Libro: Principles of Model Cheking. Cap. 6 Computation Tree Logical
http://en.wikipedia.org/wiki/Computation_tree_logic