Lógica temporal proposicional cronometrada

En la verificación de modelos , un campo de la informática , la Lógica Proposicional Temporal Programada ( TPTL ) es una extensión de la Lógica Temporal Lineal (LTL) en la que se introducen variables para medir tiempos entre dos eventos. Por ejemplo, mientras que LTL permite establecer que cada evento p es eventualmente seguido por un evento q , TPTL además permite dar un límite de tiempo para que ocurra q .

Sintaxis

El fragmento futuro de TPTL se define de manera similar a la lógica temporal lineal , en la que además, se pueden introducir variables de reloj y compararlas con constantes. Formalmente, dado un conjunto de relojes, MTL se construye a partir de:${\displaystyle X}$

• un conjunto finito de variables proposicionales AP ,
• los operadores lógicos ¬ y ∨, y
• el operador modal temporal U ,
• una comparación de reloj , con , un número y ser un operador de comparación como <, ≤, =, ≥ o>.${\displaystyle x\sim c}$${\displaystyle x\in X}$${\displaystyle c}$${\displaystyle \sim }$
• un operador de cuantificación de congelación , para una fórmula TPTL con un conjunto de relojes .${\displaystyle x.\phi }$${\displaystyle \phi }$${\displaystyle X\cup \{x\}}$

Además, para un intervalo, se considera una abreviatura de ; y de manera similar para cualquier otro tipo de intervalos.${\displaystyle I=(a,b)}$${\displaystyle x\in I}$${\displaystyle x>a\land x<b}$

La lógica TPTL + Past ^[1] se construye como el fragmento futuro de TLS y también contiene

• el operador modal temporal S .

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

Una fórmula cerrada es una fórmula sobre un conjunto de relojes vacío. ^[2]

Modelo

Dejemos que represente intuitivamente un conjunto de tiempo. Sea una función que asocie a cada momento un conjunto de proposiciones de AP . Un modelo de una fórmula TPTL 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 {\mathcal {P}}(AP)}$${\displaystyle t\in T}$${\displaystyle \gamma }$${\displaystyle \gamma }$${\displaystyle T}$

Semántico

Deja y como arriba. Dejemos un juego de relojes . Dejemos que se acabe la valoración del reloj .${\displaystyle T}$${\displaystyle \gamma }$${\displaystyle X}$${\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}$${\displaystyle X}$

Ahora vamos a explicar qué significa que una fórmula TPTL se mantenga en el momento de una valoración . Esto se denota por . Deje y ser dos fórmulas sobre el conjunto de relojes , una fórmula sobre el conjunto de relojes , , , un número y ser un operador de comparación como <, ≤, =, ≥ o>: En primer lugar, debe tener en cuenta fórmulas cuya principal operador también pertenece a LTL:${\displaystyle \phi }$${\displaystyle t}$${\displaystyle \nu }$${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \phi }$${\displaystyle \psi }$${\displaystyle X}$${\displaystyle \xi }$${\displaystyle X\cup \{y\}}$${\displaystyle x\in X}$${\displaystyle l\in {\mathtt {AP}}}$${\displaystyle c}$${\displaystyle \sim }$

• ${\displaystyle \gamma ,t,\nu \models l}$sostiene si ,${\displaystyle l\in \gamma (t)}$
• ${\displaystyle \gamma ,t,\nu \models \neg \phi }$se mantiene si o${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \lor \psi }$se mantiene si o${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi {\mathcal {U}}\psi }$sostiene si existe tal que y tal que para cada , ,${\displaystyle t<t''}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t<t'<t''}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models \phi {\mathcal {S}}\psi }$sostiene si existe tal que y tal que para cada , ,${\displaystyle t''<t}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t''<t'<t}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models y.\xi }$aguanta si aguanta,${\displaystyle \gamma ,t,\nu [y\to t]\models \phi }$
• ${\displaystyle \gamma ,t,\nu \models x\sim c}$sostiene si .${\displaystyle t-\nu (y)\sim c}$

Lógica temporal métrica

La lógica temporal métrica es otra extensión de LTL que permite medir el tiempo. En lugar de agregar variables, agrega una infinidad de operadores y para un intervalo de número no negativo. La semántica de la fórmula en algún momento es esencialmente la misma que la semántica de la fórmula , con las restricciones de que el tiempo en el que debe cumplirse ocurre en el intervalo .${\displaystyle {\mathcal {U}}_{I}}$${\displaystyle {\mathcal {S}}_{I}}$${\displaystyle I}$${\displaystyle \phi {\mathcal {U}}_{I}\psi }$${\displaystyle t}$${\displaystyle \phi {\mathcal {U}}\psi }$${\displaystyle t''}$${\displaystyle \psi }$${\displaystyle t+I}$

TPTL es tan expresivo como MTL. De hecho, la fórmula MTL es equivalente a la fórmula TPTL donde es una nueva variable. ^[2]${\displaystyle \phi {\mathcal {U}}_{I}\psi }$${\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )}$${\displaystyle x}$

De ello se deduce que cualquier otro operador introducido en la página MTL , como y también se puede definir como fórmulas TPTL.${\displaystyle \Box }$${\displaystyle \Diamond }$

TPTL es estrictamente más expresivo que MTL ^{[1] : 2} tanto sobre palabras cronometradas como sobre señales. Palabras sobre tiempo, ninguna fórmula MTL es equivalente a . Sobre la señal, no hay una fórmula MTL equivalente a , que establece que la última proposición atómica antes del punto de tiempo 1 es un .${\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))}$${\displaystyle x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))}$${\displaystyle a}$

Comparación con LTL

Una palabra infinita estándar (sin tiempo) es una función de a . Podemos considerar una palabra así usando el conjunto de tiempo y la función . En este caso, para una fórmula LTL arbitraria, si y solo si , where se considera una fórmula TPTL con un operador no estricto y es la única función definida en el conjunto vacío.${\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,\nu \models \phi }$${\displaystyle \phi }$${\displaystyle \nu }$

Referencias

1. Bouyer, Patricia ; Chevalier, Fabrice; Markey, Nicolas (2005). "Sobre la expresividad de TPTL y MTL" . Ceremonias de la 25ª Conferencia sobre Fundamentos de la Tecnología del Software y la Informática Teórica : 436. doi : 10.1007 / 11590156_3 .
2. Alur, Rajeev; Henzinger, Thomas A. (enero de 1994). "Una lógica realmente temporal". Revista de la ACM . 41 (1): 181–203. doi : 10.1145 / 174644.174651 .