Lógica temporal métrica

La lógica temporal métrica (MTL) es un caso especial de lógica temporal . Es una extensión de la lógica temporal en la que los operadores temporales se reemplazan por versiones con restricciones temporales como los operadores hasta , siguiente , desde y anterior . Es una lógica de tiempo lineal que asume tanto las abstracciones de intercalación como de reloj ficticio. Se define sobre una semántica de tiempo entero débilmente monótona basada en puntos.

Se ha descrito a MTL como un formalismo de especificación destacado para sistemas en tiempo real. ^[1] La MTL completa sobre infinitas palabras cronometradas es indecidible. ^[2]

Sintaxis

La lógica temporal métrica completa se define de manera similar a la lógica temporal lineal , donde se agrega un conjunto de números reales no negativos a los operadores modales temporales U y S. Formalmente, la MTL se construye a partir de:

• un conjunto finito de variables proposicionales AP ,
• los operadores lógicos ¬ y ∨, y
• el operador modal temporal U _I (pronunciado " φ hasta en I ψ ."), con I un intervalo de números no negativos.
• el operador modal temporal S _I (pronunciado " φ ya que en I ψ ."), con I como arriba.

Cuando se omite el subíndice, implícitamente es igual a . ${\displaystyle [0,\infty )}$

Tenga en cuenta que el siguiente operador N no se considera parte de la sintaxis MTL. En cambio, se definirá a partir de otros operadores.

Pasado y futuro

El fragmento pasado de la lógica temporal métrica , denominado past-MTL , se define como la restricción de la lógica temporal métrica completa sin el operador till. De manera similar, el fragmento futuro de la lógica temporal métrica , denominado future-MTL, se define como la restricción de la lógica temporal métrica completa sin el operador since.

Dependiendo de los autores, MTL se define como el fragmento futuro de MTL, en cuyo caso MTL completo se denomina MTL+Pasado . ^{[1] [3]} O MTL se define como MTL completo.

Para evitar ambigüedades, en este artículo se utilizan los nombres full-MTL, past-MTL y future-MTL. Cuando las afirmaciones sean válidas para las tres lógicas, se utilizará simplemente MTL.

Modelo

Representemos intuitivamente un conjunto de puntos en el tiempo. Sea una función que asocie una letra a cada momento . Un modelo de una fórmula MTL es una función de este tipo . Por lo general, es una palabra cronometrada o una señal . En esos casos, es un subconjunto discreto o un intervalo que contiene 0. ${\displaystyle T\subseteq \mathbb {R} _{+}}$ ${\displaystyle \gamma :T\to A}$ ${\displaystyle t\in T}$ ${\displaystyle \gamma }$ ${\displaystyle \gamma }$ ${\displaystyle T}$

Semántica

Sea y como se indica anteriormente y sea un tiempo fijo. Ahora vamos a explicar qué significa que una fórmula MTL se cumple en el tiempo , que se denota . ${\displaystyle T}$ ${\displaystyle \gamma }$ ${\displaystyle t\in T}$ ${\displaystyle \phi }$ ${\displaystyle t}$ ${\displaystyle \gamma ,t\models \phi }$

Sea y . Primero, consideremos la fórmula . Decimos que si y solo si existe algún tiempo tal que: ${\displaystyle I\subseteq \mathbb {R} _{+}}$ ${\displaystyle \phi ,\psi \in MTL}$ ${\displaystyle \phi {\mathcal {U}}_{I}\psi }$ ${\displaystyle \gamma ,t\models \phi {\mathcal {U}}_{I}\psi }$ ${\displaystyle t'\in I+t}$

• ${\displaystyle \gamma ,t'\models \psi }$y
• para cada uno con , . ${\displaystyle t''\in T}$ ${\displaystyle t<t''<t'}$ ${\displaystyle \gamma ,t''\models \phi }$

Consideremos ahora la fórmula (pronunciada " ya que en "). Decimos que si y sólo si existe algún tiempo tal que: ${\displaystyle \phi {\mathcal {S}}_{I}\psi }$ ${\displaystyle \phi }$ ${\displaystyle I}$ ${\displaystyle \psi }$ ${\displaystyle \gamma ,t\models \phi {\mathcal {S}}_{I}\psi }$ ${\displaystyle t'\in I-t}$

• ${\displaystyle \gamma ,t'\models \psi }$y
• para cada uno con , . ${\displaystyle t''\in T}$ ${\displaystyle t'<t''<t}$ ${\displaystyle \gamma ,t''\models \phi }$

Las definiciones de los valores no considerados anteriormente son similares a la definición en el caso LTL . ${\displaystyle \gamma ,t\models \phi }$ ${\displaystyle \phi }$

Operadores definidos a partir de operadores MTL básicos

Algunas fórmulas se utilizan con tanta frecuencia que se introduce un nuevo operador para ellas. Estos operadores no suelen considerarse parte de la definición de MTL, sino que son azúcar sintáctico que denotan una fórmula MTL más compleja. En primer lugar, consideramos los operadores que también existen en LTL. En esta sección, corregimos las fórmulas MTL y . ${\displaystyle \phi ,\psi }$ ${\displaystyle I\subseteq \mathbb {R} _{+}}$

Operadores similares a los de LTL

Liberar y volver a

Denotamos por (pronunciado " release in " ) la fórmula . Esta fórmula se cumple en el momento si: ${\displaystyle \phi {\mathcal {R}}_{I}\psi }$ ${\displaystyle \phi }$ ${\displaystyle I}$ ${\displaystyle \psi }$ ${\displaystyle \neg \phi {\mathcal {U}}_{I}\neg \psi }$ ${\displaystyle t}$

• Hay algún tiempo tal que se cumple, y se cumple en el intervalo . ${\displaystyle t'\in t+I}$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle (t,t')\cap (t+I)}$
• en cada momento , se sostiene. ${\displaystyle t'\in t+I}$ ${\displaystyle \psi }$

El nombre “liberación” proviene del caso LTL, donde esta fórmula simplemente significa que siempre debe mantenerse, a menos que se libere. ${\displaystyle \phi }$ ${\displaystyle \psi }$

La contraparte pasada de liberación se denota por (pronunciado " de vuelta a en " ) y es igual a la fórmula . ${\displaystyle \phi {\mathcal {B}}_{I}\psi }$ ${\displaystyle \phi }$ ${\displaystyle I}$ ${\displaystyle \psi }$ ${\displaystyle \neg \phi {\mathcal {S}}_{I}\neg \psi }$

Finalmente y eventualmente

Denotamos por o (pronunciado "Finalmente en , " o "Eventualmente en , ") la fórmula . Intuitivamente, esta fórmula se cumple en el tiempo si hay algún tiempo tal que se cumple. ${\displaystyle \Diamond _{I}\phi }$ ${\displaystyle {\mathcal {F}}_{I}\phi }$ ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle \top {\mathcal {U}}_{I}\phi }$ ${\displaystyle t}$ ${\displaystyle t'\in t+I}$ ${\displaystyle \phi }$

Denotamos por o (pronunciado "Globalmente en , ",) la fórmula . Intuitivamente, esta fórmula se cumple en el momento si para todo el tiempo , se cumple. ${\displaystyle \Box _{I}\phi }$ ${\displaystyle {\mathcal {G}}_{I}\phi }$ ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle \neg \Diamond _{I}\neg \phi }$ ${\displaystyle t}$ ${\displaystyle t'\in t+I}$ ${\displaystyle \phi }$

Denotamos por y la fórmula es similar a y , donde se reemplaza por . Ambas fórmulas tienen intuitivamente el mismo significado, pero cuando consideramos el pasado en lugar del futuro. ${\displaystyle {\overleftarrow {\Box }}_{I}\phi }$ ${\displaystyle {\overleftarrow {\Diamond }}_{I}\phi }$ ${\displaystyle \Box _{I}\phi }$ ${\displaystyle \Diamond _{I}\phi }$ ${\displaystyle {\mathcal {U}}}$ ${\displaystyle {\mathcal {S}}}$

Siguiente y anterior

Este caso es ligeramente diferente a los anteriores, porque el significado intuitivo de las fórmulas “Siguiente” y “Anteriormente” difiere dependiendo del tipo de función considerada. ${\displaystyle \gamma }$

Denotamos por o (pronunciado "Next in , ") la fórmula . De manera similar, denotamos por ^[4] (pronunciado "Previously in , ") la fórmula . La siguiente discusión sobre el operador Next también es válida para el operador Previously, al invertir el pasado y el futuro. ${\displaystyle \bigcirc _{I}\phi }$ ${\displaystyle {\mathcal {N}}_{I}\phi }$ ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle \bot {\mathcal {U}}_{I}\phi }$ ${\displaystyle \ominus _{I}\phi }$ ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle \bot {\mathcal {S}}_{I}\phi }$

Cuando esta fórmula se evalúa sobre una palabra cronometrada , significa que: ${\displaystyle \gamma :T\to A}$

• En la próxima ocasión en el dominio de definición , la fórmula será válida. ${\displaystyle T}$ ${\displaystyle \phi }$
• Además, la distancia entre esta próxima vez y la hora actual pertenece al intervalo . ${\displaystyle I}$
• En particular, este próximo tiempo se cumple, por lo tanto el tiempo actual no es el final de la palabra.

Cuando se evalúa esta fórmula sobre una señal , la noción de siguiente momento no tiene sentido. En cambio, "siguiente" significa "inmediatamente después". Más precisamente significa: ${\displaystyle \gamma }$ ${\displaystyle \gamma ,t\models \circ \phi }$

• ${\displaystyle I}$contiene un intervalo de la forma y ${\displaystyle (0,\epsilon )}$
• para cada , . ${\displaystyle t'\in (t,t+\epsilon )}$ ${\displaystyle \gamma ,t'\models \phi }$

Otros operadores

Ahora consideraremos operadores que no son similares a ningún operador LTL estándar.

Caída y ascenso

Denotamos por (pronunciado "rise ") una fórmula que se cumple cuando se vuelve verdadera. Más precisamente, o bien no se cumplió en el pasado inmediato y se cumple en este momento, o bien no se cumple y se cumple en el futuro inmediato. Formalmente se define como . ^[5] ${\displaystyle \uparrow \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \uparrow \phi }$ ${\displaystyle (\phi \land (\neg \phi {\mathcal {S}}\top ))\lor (\neg \phi \land (\phi {\mathcal {U}}\top ))}$

Con el paso del tiempo, esta fórmula siempre se cumple. De hecho, y siempre se cumple. Por lo tanto, la fórmula es equivalente a , por lo tanto es verdadera. ${\displaystyle \phi {\mathcal {U}}\top }$ ${\displaystyle \neg \phi {\mathcal {S}}\top }$ ${\displaystyle \phi \lor \neg \phi }$

Por simetría, denotamos por (pronunciado "Fall" ), una fórmula que se cumple cuando se vuelve falsa. Por lo tanto, se define como . ${\displaystyle \downarrow \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle (\neg \phi \land (\phi {\mathcal {S}}\top ))\land (\phi \land (\neg \phi {\mathcal {U}}\top ))}$

Historia y profecía

Introducimos ahora el operador de profecía , denotado por . Denotamos por ^[6] la fórmula . Esta fórmula afirma que existe un primer momento en el futuro tal que se cumple, y el tiempo de espera para este primer momento pertenece a . ${\displaystyle \triangleright }$ ${\displaystyle \triangleright _{I}\phi }$ ${\displaystyle \neg \phi {\mathcal {U}}_{I}\phi }$ ${\displaystyle \phi }$ ${\displaystyle I}$

Ahora consideramos esta fórmula sobre palabras cronometradas y sobre señales. Consideramos primero las palabras cronometradas. Supongamos que donde y representa límites abiertos o cerrados. Sea una palabra cronometrada y en su dominio de definición. Sobre palabras cronometradas, la fórmula se cumple si y solo si también se cumple. Es decir, esta fórmula simplemente afirma que, en el futuro, hasta que se cumpla el intervalo, no debería cumplirse. Además, debería cumplirse en algún momento en el intervalo . De hecho, dado cualquier momento tal que se cumpla, solo existe un número finito de tiempo con y . Por lo tanto, existe necesariamente un menor tal . ${\displaystyle I=\mid a,b\mid '}$ ${\displaystyle \mid }$ ${\displaystyle \mid '}$ ${\displaystyle \gamma }$ ${\displaystyle t}$ ${\displaystyle \gamma ,t\models \triangleright _{I}\phi }$ ${\displaystyle \gamma ,t\models \Box _{]0,b[\setminus I}\neg \phi \land \Diamond _{I}\phi }$ ${\displaystyle t+I}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle t+I}$ ${\displaystyle t''\in t+I}$ ${\displaystyle \gamma ,t''\models \phi }$ ${\displaystyle t'\in t+I}$ ${\displaystyle t'<t''}$ ${\displaystyle \gamma ,t'\models \phi }$ ${\displaystyle t''}$

Consideremos ahora la señal. La equivalencia mencionada anteriormente ya no se cumple en el caso de la señal. Esto se debe a que, utilizando las variables introducidas anteriormente, puede existir un número infinito de valores correctos para , debido a que el dominio de definición de una señal es continuo. Por lo tanto, la fórmula también garantiza que el primer intervalo en el que se cumple esté cerrado por la izquierda. ${\displaystyle t'}$ ${\displaystyle \triangleright _{I}\phi }$ ${\displaystyle \phi }$

Por simetría temporal, definimos el operador de historia , denotado por . Definimos como . Esta fórmula afirma que existe un último momento en el pasado tal que se mantuvo. Y el tiempo transcurrido desde este primer momento pertenece a . ${\displaystyle \triangleleft }$ ${\displaystyle \triangleleft _{I}\phi }$ ${\displaystyle \neg \phi {\mathcal {S}}_{I}\phi }$ ${\displaystyle \phi }$ ${\displaystyle I}$

Operador no estricto

La semántica de los operadores hasta y desde introducidos no considera el tiempo actual. Es decir, para que to se cumpla en algún momento , ni ni tiene que cumplirse en el momento . Esto no siempre es lo que se desea, por ejemplo, en la oración "no hay ningún error hasta que se apague el sistema", puede que en realidad se desee que no haya ningún error en el momento actual. Por lo tanto, introducimos otro operador hasta , llamado no estricto hasta , denotado por , que considera el tiempo actual. ${\displaystyle \phi _{1}{\mathcal {U}}\phi _{2}}$ ${\displaystyle t}$ ${\displaystyle \phi _{1}}$ ${\displaystyle \phi _{2}}$ ${\displaystyle t}$ ${\displaystyle {\overline {\mathcal {U}}}}$

Denotamos por y ya sea: ${\displaystyle \phi _{1}{\overline {\mathcal {U}}}_{I}\phi _{2}}$ ${\displaystyle \phi _{1}{\overline {\mathcal {S}}}_{I}\phi _{2}}$

• las fórmulas y si , y ${\displaystyle \phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2}))}$ ${\displaystyle \phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2}))}$ ${\displaystyle 0\in I}$
• las fórmulas y demás. ${\displaystyle \phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2})}$ ${\displaystyle \phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2})}$

Para cualquiera de los operadores introducidos anteriormente, denotamos la fórmula en la que se utilizan hasta y desde no estrictos. Por ejemplo, es una abreviatura de . ${\displaystyle {\mathcal {O}}}$ ${\displaystyle {\overline {\mathcal {O}}}}$ ${\displaystyle {\overline {\Diamond }}p}$ ${\displaystyle \top {\overline {\mathcal {U}}}p}$

El operador estricto no se puede definir utilizando un operador no estricto. Es decir, no existe una fórmula equivalente a la que utilice únicamente un operador no estricto. Esta fórmula se define como . Esta fórmula nunca puede cumplirse en un momento dado si se requiere que se cumpla en el momento . ${\displaystyle \bigcirc _{I}p}$ ${\displaystyle \bot {\mathcal {U}}_{I}p}$ ${\displaystyle t}$ ${\displaystyle \bot }$ ${\displaystyle t}$

Ejemplo

A continuación, se ofrecen ejemplos de fórmulas MTL. Se pueden encontrar más ejemplos en el artículo sobre fragmentos de MITL, como la lógica temporal de intervalos métricos .

• ${\displaystyle \Box (p\implies \Diamond _{\{1\}}q)}$establece que cada letra es seguida exactamente una unidad de tiempo después por una letra . ${\displaystyle p}$ ${\displaystyle q}$
• ${\displaystyle \Box (p\implies \neg \Diamond _{\{1\}}p)}$establece que no pueden ocurrir dos ocurrencias sucesivas de exactamente con una unidad de tiempo de diferencia. ${\displaystyle p}$

Comparación con LTL

Una palabra infinita estándar (sin tiempo) es una función de a . Podemos considerar una palabra de este tipo utilizando el conjunto de tiempo y la función . En este caso, para una fórmula LTL arbitraria, si y solo si , donde se considera una fórmula MTL con operador no estricto y subíndice. En este sentido, MTL es una extensión de LTL. ^{[ aclaración necesaria ]} ${\displaystyle w=a_{0},a_{1},\dots ,}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle A}$ ${\displaystyle T=\mathbb {N} }$ ${\displaystyle \gamma (i)=a_{i}}$ ${\displaystyle \phi }$ ${\displaystyle w,i\models \phi }$ ${\displaystyle \gamma ,i\models \phi }$ ${\displaystyle \phi }$ ${\displaystyle [0,\infty )}$

Por este motivo, una fórmula que utiliza únicamente un operador no estricto con subíndice se denomina fórmula LTL. Esto se debe a que ^{[ se necesita más explicación ]} ${\displaystyle [0,\infty )}$

Complejidad algorítmica

La satisfacibilidad de ECL sobre señales es EXPSPACE - completa . ^[6]

Fragmentos de MTL

Consideremos ahora algunos fragmentos de MTL.

MITL

Un subconjunto importante de MTL es la lógica temporal de intervalos métricos ( MITL ). Esta se define de manera similar a MTL, con la restricción de que los conjuntos , utilizados en y , son intervalos que no son singletons y cuyos límites son números naturales o infinitos. ${\displaystyle I}$ ${\displaystyle {\mathcal {U}}}$ ${\displaystyle {\mathcal {S}}}$

Algunos otros subconjuntos de MITL se definen en el artículo MITL .

Fragmentos futuros

El Future-MTL ya se presentó anteriormente. Tanto en el caso de las palabras cronometradas como de las señales, es menos expresivo que el Full-MTL ^{[3] : 3} .

Lógica temporal del reloj de eventos

El fragmento Event-Clock Temporal Logic ^[6] de MTL, denominado EventClockTL o ECL , permite únicamente los siguientes operadores:

• los operadores booleanos, y, o, no
• los operadores hasta y desde no cronometrados.
• Los operadores de la profecía cronometrada y la historia.

En cuanto a las señales, ECL es tan expresivo como MITL y como MITL ₀ . La equivalencia entre las dos últimas lógicas se explica en el artículo MITL ₀ . Esbozamos la equivalencia de esas lógicas con ECL.

Si no es un singleton y es una fórmula MITL, se define como una fórmula MITL. Si es un singleton, entonces es equivalente a que es una fórmula MITL. Recíprocamente, para una fórmula ECL y un intervalo cuyo límite inferior es 0, es equivalente a la fórmula ECL . ${\displaystyle I}$ ${\displaystyle \phi }$ ${\displaystyle \triangleright _{I}\phi }$ ${\displaystyle I=\{i\}}$ ${\displaystyle \triangleright _{I}\phi }$ ${\displaystyle \Box _{]0,i[}\neg \phi \land \Diamond _{]0,i]}\phi }$ ${\displaystyle \psi }$ ${\displaystyle I}$ ${\displaystyle \Box _{I}\psi }$ ${\displaystyle \neg \triangleright _{I}\neg \psi }$

La satisfacibilidad de ECL sobre señales es PSPACE-completa . ^[6]

Forma normal positiva

Una fórmula MTL en forma normal positiva se define casi como cualquier fórmula MTL, con los dos cambios siguientes:

• Los operadores Release y Back se introducen en el lenguaje lógico y ya no se consideran notaciones para otras fórmulas.
• Las negaciones sólo se pueden aplicar a las letras.

Cualquier fórmula MTL es equivalente a una fórmula en forma normal. Esto se puede demostrar mediante una inducción sencilla sobre fórmulas. Por ejemplo, la fórmula es equivalente a la fórmula . De manera similar, las conjunciones y disyunciones se pueden considerar utilizando las leyes de De Morgan . ${\displaystyle \neg (\phi {\mathcal {U}}_{S}\psi )}$ ${\displaystyle (\neg \phi ){\mathcal {R}}_{S}(\neg \psi )}$

Estrictamente hablando, el conjunto de fórmulas en forma normal positiva no es un fragmento de MTL.

Véase también

• Lógica temporal proposicional cronometrada , otra extensión de la LTL en la que se puede medir el tiempo.

Referencias

1. J. Ouaknine y J. Worrell, "Sobre la decidibilidad de la lógica temporal métrica", 20º Simposio Anual IEEE sobre Lógica en Ciencias de la Computación (LICS' 05), 2005, págs. 188-197.
2. Ouaknine J., Worrell J. (2006) Sobre lógica temporal métrica y máquinas de Turing defectuosas. En: Aceto L., Ingólfsdóttir A. (eds) Fundamentos de la ciencia del software y estructuras computacionales. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlín, Heidelberg
3. Bouyer, Patricia ; Chevalier, Fabrice; Markey, Nicolas (2005). "Sobre la expresividad de TPTL y MTL". En Sundar Sarukkai; Sandeep Sen (eds.). FSTTCS 2005: Fundamentos de la tecnología de software y la ciencia informática teórica, Actas . 25.ª Conferencia internacional, Hyderabad, India, 15-18 de diciembre de 2005. Lecture Notes in Computer Science. Vol. 3821. pág. 436. doi :10.1007/11590156_35. ISBN 978-3-540-32419-5.
4. Maler, Oded; Nickovic, Dejan; Pnueli, Amir (2008). "Comprobación de propiedades temporales de comportamientos discretos, cronometrados y continuos". Pilares de la informática . ACM. pág. 478. ISBN 978-3-540-78126-4.
5. Nickovic, Dejan (31 de agosto de 2009). "3". Comprobación de propiedades temporizadas e híbridas: teoría y aplicaciones (tesis).
6. Henzinger, TA; Raskin, JF; Schobbens, P.-Y. (1998). "Los lenguajes regulares de tiempo real". Autómatas, lenguajes y programación . Apuntes de clase en informática. Vol. 1443. pág. 590. doi :10.1007/BFb0055086. ISBN. 978-3-540-64781-2.