lógica temporal proposicional cronometrada

En la verificación de modelos , un campo de la informática , la lógica temporal proposicional temporizada ( TPTL ) es una extensión de la lógica temporal lineal proposicional (LTL) en la que se introducen variables para medir el tiempo entre dos eventos. Por ejemplo, mientras que LTL permite afirmar que cada evento p es seguido eventualmente por un evento q , TPTL permite además establecer un límite de tiempo para que ocurra q .

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${\displaystyle X}$MTL , compuesto por relojes, se construye a partir de:

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

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

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

• el operador modal temporal S .

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 vacío de relojes. ^{[ 2 ]}

Dejar${\displaystyle T\subseteq \mathbb {R} _{+}}$, que intuitivamente representa un conjunto de tiempos. Sea${\displaystyle \gamma :T\to {\mathcal {P}}(AP)}$una función que se asocia a cada momento${\displaystyle t\in T}$un conjunto de proposiciones de AP . Un modelo de una fórmula TPTL es una función de este tipo.${\displaystyle \gamma }$. Generalmente,${\displaystyle \gamma }$es una palabra temporizada o una señal . En esos casos,${\displaystyle T}$es un subconjunto discreto o un intervalo que contiene 0.

Dejar${\displaystyle T}$y${\displaystyle \gamma }$Sea como arriba. Que${\displaystyle X}$Sea un conjunto de relojes .${\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}$(una valoración del reloj más de${\displaystyle X}$).

Ahora vamos a explicar qué significa para una fórmula TPTL.${\displaystyle \phi }$para sostener en el momento${\displaystyle t}$para una valoración${\displaystyle \nu }$Esto se denota por${\displaystyle \gamma ,t,\nu \modelos \phi }$. Dejar${\displaystyle \phi }$y${\displaystyle \psi }$sean dos fórmulas sobre el conjunto de relojes${\displaystyle X}$,${\displaystyle \xi }$una fórmula sobre el conjunto de relojes${\displaystyle X\cup \{y\}}$,${\displaystyle x\in X}$, ${\displaystyle l\in {\mathtt {AP}}}$,${\displaystyle c}$un número y${\displaystyle \sim }$siendo un operador de comparación como < , ≤ , =, ≥ o > : Primero consideramos fórmulas cuyo operador principal también pertenece a LTL:

• ${\displaystyle \gamma ,t,\nu \modelos l}$se sostiene si${\displaystyle l\in \gamma (t)}$,
• ${\displaystyle \gamma ,t,\nu \models \neg \phi }$se sostiene si${\displaystyle \gamma ,t,\nu \not \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \lor \psi }$se cumple si alguna de las${\displaystyle \gamma ,t,\nu \modelos \phi }$o${\displaystyle \gamma ,t,\nu \models \psi }$o ambas
• ${\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi }$se sostiene si existe${\displaystyle t''}$de tal manera que${\displaystyle t<t''}$y${\displaystyle \gamma ,t'',\nu \modelos \psi }$y para cada${\displaystyle t'}$con${\displaystyle t<t'<t''}$, ${\displaystyle \gamma ,t',\nu \models \phi }$,
• ${\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {S}} \psi }$se sostiene si existe${\displaystyle t''}$de tal manera que${\displaystyle t''<t}$y${\displaystyle \gamma ,t'',\nu \modelos \psi }$y para cada${\displaystyle t'}$con ${\displaystyle t''<t'<t}$, ${\displaystyle \gamma ,t',\nu \models \phi }$,
• ${\displaystyle \gamma ,t,\nu \models x\sim c}$se sostiene si${\displaystyle t-\nu (y)\sim c}$,
• ${\displaystyle \gamma ,t,\nu \models y.\xi }$se sostiene si${\displaystyle \gamma ,t,\nu [y\to t]\models \phi }$sostiene.

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

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

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

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

Una palabra infinita estándar (sin límite de tiempo)${\displaystyle w=a_{0},a_{1},\dots ,}$es una función de${\displaystyle \mathbb {N} }$a${\displaystyle A}$Podemos considerar dicha palabra utilizando el conjunto de tiempo${\displaystyle T=\mathbb {N} }$y la función${\displaystyle \gamma (i)=a_{i}}$. En este caso, para${\displaystyle \phi }$una fórmula LTL arbitraria,${\displaystyle w,i\models \phi }$si y solo si${\displaystyle \gamma ,i,\nu \models \phi }$, dónde${\displaystyle \phi }$se considera una fórmula TPTL con operador no estricto, y${\displaystyle \nu }$es la única función definida en el conjunto vacío.