T11. Lógica temporal lineal LTL

Está semana la tarea consistio en:

Elegir un inciso de los ejercicios del capitulo 14 Linear Temporal Logic LTL
yo elegí el 14.3.2

Como nos menciona el libro encontramos

What are the properties expressed by the following LTL formulas?
¿Cuáles son las propiedades expresadas por las siguente formula LTL?

Aquí encontramos los siguientes operadores: 

Por lo tanto la propiedad expresada quedaría de la siguente manera: 

• Siempre hay A  implicado en la siguente A. 
• Siempre hay  un estado A implicado en el siguiente estado A. 

Referencias: 

LTL

Link2

T10. Propiedades de modelos de verificación

La tarea en esta semena consistio en:

• Inventen una expresión ω-regular con por lo menos dos símbolos y por lo menos dos operadores.
• Dibujen el NBA que le corresponde.

Como ya antes vimos las propiedades pueden ser: 

• Deterministas 
• No Deterministas

Esta sería la expresión a representar :
(W + XY*V)*XY*

Los operadores utilizan diferentes funciones:
Asterisco(*): Esto es cuando algo se repiten  0 o mas veces.
Suma(+): Sirve para encontrar una cadena repetida.

Concatenación:

 Unión: 

Retorno: 

Referencias:
http://web.ing.puc.cl/~marenas/iic3800/clases/automata-1-imp.pdf