T12: Linear Temporal Logic

Como vimos en los ejemplos de maquina vending en clase, podemos formular la operación de recarga que se hace infinitas veces, debemos de satisfacer algunas propiedades, por lo que en base a esto realizamos desarrollamos el ejercicio.

Podemos ver que tenemos los siguientes operadores temporales y los conectivos:

Obtenida de LTS capítulo 14

Se nos pide formalizar la siguiente oración acerca de la maquina vending en LTL.

3) The recharge transaction occurs infinitely often.

Podemos expresar como T la operación de recarga, entonces, para decir que esta operación ocurre infinitamente utilizaremos los operadores temporales:

□   =    siempre

◇   =     eventualmente

Por lo tanto expresamos con T la operación de recarga,  para concluir que.

□◇T

Bibliografía
Capítulo 14 LTL Link