Lógica Temporal

Verificación y Validación de Software
Entrada 11

Para esta semana seleccionamos un ejercicio del PDF mencionado al final de esta publicación, referente a lógica lineal temporal (LTL, por sus siglas en inglés).

El ejercicio seleccionado fue el 14.1.6 y la traducción literal del enunciado es el siguiente.

Si un estudiante olvida una moneda en la ranura de monedas, otro estudiante usará esta moneda para obtener una bebida antes de que cualquier profesor pueda hacerlo.

Entonces usando los operadores temporales tenemos:

$\square (eom \Rightarrow \circ(¬pum \ R \ eum))$

Donde:
eom = Estudiante Olvida Moneda
pum = Profesor Usa Moneda
eum = Estudiante Usa Moneda

Recursos consultados:
Linear Temporal Logic