Lógica temporal de intervalo métrico

Fragmento de lógica temporal métrica

En la verificación de modelos , la lógica temporal de intervalo métrico (MITL) es un fragmento de la lógica temporal métrica (MTL). Este fragmento suele preferirse a la MTL porque algunos problemas que no se pueden decidir con MTL se pueden decidir con MITL.

Definición

Una fórmula MITL es una fórmula MTL, de modo que cada conjunto de números reales utilizados en subíndice son intervalos, que no son singletons, y cuyos límites son un número natural o son infinitos. ^{[ cita requerida ]}

Diferencia con MTL

La MTL puede expresar una afirmación como la oración S : " P se mantuvo hace exactamente diez unidades de tiempo". Esto es imposible en MITL. En cambio, MITL puede decir T : " P se mantuvo hace entre 9 y 10 unidades de tiempo". Dado que MITL puede expresar T pero no S , en cierto sentido, MITL es una restricción de la MTL que solo permite afirmaciones menos precisas.

Problemas que MITL evita

Una razón para querer evitar un enunciado como S es que su valor de verdad puede cambiar un número arbitrario de veces en una sola unidad de tiempo. De hecho, el valor de verdad de este enunciado puede cambiar tantas veces como cambie el valor de verdad de P , y P en sí mismo puede cambiar un número arbitrario de veces en una sola unidad de tiempo.

Consideremos ahora un sistema, como un autómata cronometrado o un autómata de señales , que desea saber en cada instante si S se cumple o no. Este sistema debería recordar todo lo que ocurrió en las últimas 10 unidades de tiempo. Como se vio anteriormente, esto significa que debe recordar un número arbitrario de eventos. Esto no puede implementarse mediante un sistema con memoria y relojes finitos.

Variabilidad limitada

Una de las principales ventajas de MITL es que cada operador tiene la propiedad de variabilidad acotada. Ejemplo:

Dada la afirmación T definida anteriormente, cada vez que el valor de verdad de T cambia de falso a verdadero, sigue siendo verdadero durante al menos una unidad de tiempo. Demostración: En un momento t en el que T se vuelve verdadero, significa que:

• Hace entre 9 y 10 unidades de tiempo, P era verdadero.
• Justo antes del tiempo t , P era falsa.

Por lo tanto, P era verdadera exactamente hace 9 unidades de tiempo. De ello se deduce que, para cada , en el tiempo , P era verdadera hace unidades de tiempo. Puesto que , en el tiempo , T se cumple. ${\displaystyle t'\in [0,1]}$ ${\displaystyle t+t'}$ ${\displaystyle 9+t'}$ ${\displaystyle 9+t'\in [9,10]}$ ${\displaystyle t'}$

Un sistema, en cada instante, desea conocer el valor de T. Dicho sistema debe recordar lo que ocurrió durante las últimas diez unidades de tiempo. Sin embargo, gracias a la propiedad de variabilidad limitada, debe recordar como máximo 10 unidades de tiempo cuando T se vuelve verdadero. Y, por lo tanto, 11 veces cuando T se vuelve falso. Por lo tanto, este sistema debe recordar como máximo 21 eventos y, por lo tanto, puede implementarse como un autómata temporizado o un autómata de señales .

Ejemplos

Ejemplos de fórmulas MITL:

• ${\displaystyle \square \diamond _{(0,1)}p}$indica que la letra aparece al menos una vez en cada intervalo abierto de longitud 1. ${\displaystyle p}$
• ${\displaystyle \triangleright _{\{i\}}p}$¿Dónde se define el operador de profecía como y que establece que la primera aparición de en el futuro está en la unidad de tiempo? ${\displaystyle \triangleright _{\{i\}}p}$ ${\displaystyle \square _{(0,i)}\neg p\land \diamond _{(0,i]}p}$ ${\displaystyle p}$ ${\displaystyle i}$
• ${\displaystyle p\land \square (p\implies \triangleright _{\{1\}}p)}$establece que esto se cumple exactamente en cada tiempo integral y no en ningún otro momento. ${\displaystyle p}$

Fragmentos

Seguridad-MTL0,∞

El fragmento Safety-MTL _0,v se define como el subconjunto de MITL _0,∞ que contiene únicamente fórmulas en forma normal positiva donde el intervalo de cada operador hasta tiene un límite superior. Por ejemplo, la fórmula que establece que a cada uno le sigue, menos de una unidad de tiempo después, un , pertenece a esta lógica. ^[1] ${\displaystyle \Box (a\implies \Diamond _{(0,1]}b)}$ ${\displaystyle a}$ ${\displaystyle b}$

MITL abierto y cerrado

El fragmento Open-MTL contiene la fórmula en forma normal positiva tal que:

• para cada , está abierto, y ${\displaystyle {\mathcal {U}}_{I}}$ ${\displaystyle I}$
• para cada , está cerrado. ${\displaystyle {\mathcal {R}}_{I}}$ ${\displaystyle I}$

El fragmento Closed-MITL contiene la negación de las fórmulas de Open-MITL .

MITL plano y coplano

El fragmento Flat-MTL contiene la fórmula en forma normal positiva tal que:

• Para cada , si no tiene límites, entonces es una fórmula LTL. ${\displaystyle \phi _{1}{\mathcal {U}}_{I}\phi _{2}}$ ${\displaystyle I}$ ${\displaystyle \phi _{1}}$
• Para cada , si no tiene límites, entonces es una fórmula LTL. ${\displaystyle \phi _{1}{\mathcal {R}}_{I}\phi _{2}}$ ${\displaystyle I}$ ${\displaystyle \phi _{2}}$

El fragmento Coflat-MITL contiene la negación de las fórmulas de Flat-MITL .

Variante no estricta

Dado cualquier fragmento L , el fragmento L ^ns es la restricción de L en la que sólo se utilizan operadores no estrictos .

MITL0,∞y MITL0

Dado cualquier fragmento L , el fragmento L _0,∞ es el subconjunto de L donde el límite inferior de cada intervalo es 0 o el límite superior es infinito. De manera similar, denotamos por L ₀ (respectivamente, L _∞ ) el subconjunto de L tal que el límite inferior de cada intervalo es 0 (respectivamente, el límite superior de cada intervalo es ∞).

Expresividad sobre señales

En las señales , MITL ₀ es tan expresivo como MITL. Esto se puede demostrar aplicando las siguientes reglas de reescritura a una fórmula MITL. ^[2]

• ${\displaystyle \phi {\mathcal {U}}_{(a,b)}\psi }$es equivalente a (la construcción para intervalos semicerrados y cerrados es similar). ${\displaystyle \Box _{(0,a]}\phi {\mathcal {U}}\psi \land \Diamond _{(a,b)}\psi }$
• ${\displaystyle \Diamond _{(a,b)}\phi }$es equivalente a si . ${\displaystyle \Diamond _{(2a-b,a)}\Box _{(0,b-a)}\Diamond _{(0,b-a)}\phi }$ ${\displaystyle 2a-b\geq 0}$
• ${\displaystyle \Diamond _{(a,b)}\phi }$es equivalente a si . ${\displaystyle \Diamond _{(a,b-a)}\Diamond _{(0,a)}\phi }$ ${\displaystyle a<b}$
• ${\displaystyle \Diamond _{(a,+\infty )}\phi }$es equivalente a . ${\displaystyle \Box _{(0,a)}\Diamond \phi }$

La aplicación de esas reglas de reescritura aumenta exponencialmente el tamaño de la fórmula. De hecho, los números y se escriben tradicionalmente en binario, y esas reglas deberían aplicarse varias veces. ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle O\left({\frac {b}{b-a}}\right)}$

Expresividad sobre palabras cronometradas

Al contrario que en el caso de las señales, MITL es estrictamente más expresivo que MITL _0,∞ . Las reglas de reescritura dadas anteriormente no se aplican en el caso de palabras cronometradas porque, para reescribir, se debe suponer que ocurre algún evento entre los tiempos 0 y , lo que no es necesariamente el caso. ${\displaystyle \Diamond _{(a,b)}}$ ${\displaystyle a}$

Problema de satisfacibilidad

El problema de decidir si una fórmula MITL es satisfactoria sobre una señal es de naturaleza PSPACE-completo . ^[3]

Referencias necesarias

R. Alur, T. Feder y TA Henzinger. Los beneficios de relajar la puntualidad. Journal of the ACM, 43(1):116–146, 1996. R. Alur y TA Henzinger. Lógicas y modelos de tiempo real: una encuesta. En Proc. REX Workshop, Tiempo real: teoría en la práctica, páginas 74–106. LNCS 600, Springer, 1992. TA Henzinger. Es cuestión de tiempo: revisión de lógicas en tiempo real. En Proc. CONCUR'98, páginas 439–454. LNCS 1466, Springer, 1998.

Referencias

1. Bulychev, Peter; David, Alexandre; Larsen, Kim G.; Guangyuan, Li (junio de 2014). "Síntesis de controlador eficiente para un fragmento de MTL _0,∞ ". Acta Informatica . 51 (3–4): 166. doi :10.1007/s00236-013-0189-z. S2CID  253779696.
2. Bersani, Marcello; Rossi, Matteo; San Pietro, Pierluigi (2013). "Una herramienta para decidir la satisfacibilidad de la lógica temporal métrica de tiempo continuo" (PDF) . 2013 20.º Simposio Internacional sobre Representación y Razonamiento Temporal . Vol. 20. pág. 202. doi :10.1109/TIME.2013.20. hdl : 11311/964235 . ISBN. 978-1-4799-2240-6.
3. 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. 591. doi :10.1007/BFb0055086. ISBN. 978-3-540-64781-2.