Lógica temporal lineal LTL

Sabemos que la máquina que provee los productos debe de ser recargada siempre que se termine el producto.

Esto puede formularse de la siguiente manera: la operación de recarga se produce un número infinito de veces. En un sistema con este tipo de limitaciones el sistema debe pasar por un estado que satisface alguna propiedad.
En el ejemplo de la maquina de productos, podemos tener este tipo de sistema por ejemplo decimos que los estudiantes compradores son infinitos.

El ejercicio que elegí es el siguiente:

EXERCISE 14.1 Formalize the following statements.


2. The beer storage becomes empty infinitely many times.

Entonces tenemos los siguientes conectivos y operadores temporales:

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

Expresamos con "Y", "que la maquina se vacía , para decir que se vacía infinitamente usaremos los siguientes operadores temporales:

 Siempre

 Next

 Eventualmente

Expresamos con "Y", "que la maquina se vacía , para decir que se vacía infinitamente usaremos los siguientes operadores temporales:

Referencias

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