Tarea 11 - Lógica temporal lineal LTL

Introducción 

Reachability and safety properties. Un estado se llama alcanzable si existe un camino cálculo de un estado inicial que conduce a este estado. La accesibilidad es una de las propiedades más importantes de los sistemas de transición en relación con las propiedades de seguridad. Supongamos que inseguro es una fórmula que expresa una propiedad indeseable de un sistema de transición. Estados cumplan inseguro se llaman inseguro o malo. A continuación, el sistema es seguro si no se puede llegar a un estado en el que tiene poco seguras. Naturalmente, nos gustaría saber si el sistema es seguro.

Mutual exclusion. La exclusión mutua se formula generalmente como una propiedad de sistemas concurrentes. Se produce cuando dos o más procesos no están autorizados a entrar en la misma sección crítica de un sistema concurrente simultáneamente.

Deadlock. Hablando muy en general, un programa concurrente está en una situación de bloqueo, cuando estado del terminal no se alcanza, sin embargo, ninguna parte del programa es capaz de proceder. Una transición sistema o sistema de transición se dice que es libre de punto muerto si no cálculo en que conduce a una callejón sin salida.

Termination and finiteness. Incluso si no tenemos una noción de un estado terminal, se puede definir los estados terminales como aquellas de las que no es posible transición. Un sistema de transición o sistema de transición es llamada de terminación, si cada cálculo en lo lleva a un estado terminal. Terminación de un sistema de transición es equivalente a la finitud de todas las rutas de cálculo, por lo que "Konig’s
Lemma" es equivalente a la finitud de cada árbol de cómputo a partir de un estado inicial. pero una camino cálculo es finito si y sólo si contiene un estado de estancamiento.

Fairness. Los cálculos arbitrarios de un sistema de transición, sabemos que algunos de estos cálculos son imposibles. Esto puede formularse de la siguiente manera: en cada camino cálculo, la operación de recarga se produce número infinito de veces. Este tipo de restricciones impuestas en el sistema: el sistema debe pasar de vez en vez a través de un estado que satisface alguna propiedad, se denomina restricción de la justicia y la equidad cálculos que cumplan las restricciones son llamados justos.

Responsiveness. A menudo es el caso en los sistemas concurrentes que un proceso envía peticiones que tienen que ser reconocidos (o respondió a) por otros procesos. Para tales sistemas que estamos interesados ​​en la propiedad de respuesta: si cada solicitud es finalmente reconocido.

Problema

Para esta semana toco elegir uno de los problemas del pdf y si contenía incisos entonces elegías uno. En mi caso mi problema tenia 4 incisos.

EXERCISE 14.7 Consider a transition system with the following state transition graph.

Which of the following formulas are true on all paths?

Para mi caso elegí el 2) pero también como algo extra hice los demás para comprobarlos también.

Explain your answer.

Respuesta

14.3 Expressing Properties of Transition Systems in LTL

Tenemos operadores temporales para cada paréntesis. 
Basándonos en los significados de cada símbolo de acuerdo a la tabla, vamos a obtener un significado de cada uno de los paréntesis: 

1) Tipo: Reachability and safety properties

Nos dice que "siempre x=0 o y=0"
Si vemos todos los caminos se cumplen en 2 casos, en el de arriba donde y = 0 y en el de la derecha donde x=0. Y en el de la izquierda nos dice que x=0 y y=0, en este caso no se cumple y que nos dice que "x=0 y y=0". Nosotros solo buscábamos uno u otro.


2) Tipo: Reachability and safety properties

Nos dice que "siempre si x = 1 entonces y = 1"
Si vemos los caminos solamente en el de arriba x=1 y no se cumple que y=1, para los demás tenemos que x=0, entonces ya y no tendría que ser 1.
Concluimos que para el único caso que x=1, y no cumple la condición.

3) Tipo: Fairness

En este tipo se habla sobre los casos infinitos, se dice que es difícil encontrar estos casos ya que se requiere que un evento ocurra casi siempre lo que dejaría de hacerlos infinitos.
Cuando tenemos los dos símbolos juntos de "siempre" y "eventualmente"  expresa que los función tiene caminos y es infinito.

En este caso decimos que "Los caminos son infinitos cuando y = 0".
Si observamos los el camino empezando desde arriba podemos ver que se pueden seguir 2 camios, uno que lleva al circulo de la derecha y otro al de la izquierda, en este caso seguimos el camino de la izquierda donde y=0 cumpliendo con la condición. Si seguimos siempre esos mismos caminos tenemos que en todos los casos se cumple y=0.



4) Tipo: Fairness

En este caso decimos que "Los caminos son infinitos cuando y=1"
Si vemos nuestro diagrama solamente en el circulo de la derecha tenemos que y=1, por lo tanto los demás caminos ya no cumplen con esta sentencia.

Bibliografía  

http://www.tcs.hut.fi/Studies/T-79.231/2003/slides5.pdf
http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14