Lógica temporal

Lógica temporal

La lógica temporal es una extención de la lógica modal , en donde el tiempo esta presente.
Los principales operadores para la lógica temporal son los siguientes:

Problema 14.1.5

(5) Professors sometimes leave with a drink left in the dispenser.

Para este problema usaremos dos variables "a" para representar a los profesores y "b" para representar "dejaron una bebida en el deposito".

Quedaría de la siguiente manera:

a ◇ b

Liga: http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14

w-Regular

En esta ocación inventaremos una expreción w-regular y la expresaremos en forma NBA

Estas son las característica que debe tener nuestra expreción: 

1-. Por lo menos dos símbolos

2-. Por lo menos dos operadores

Aquí la expreción:

Posteriormente teniendo la expreción se mostrara en un diagrama de NBA(Nondeterministic Büchi Automaton)  

Aqui el diagrama NBA:

Referencias:
Principles of model checking book
Autor: Christel Baier and Joost-Pieter Katoen