CTL*

CTL* es un superconjunto de la lógica de árbol computacional (CTL) y la lógica temporal lineal (LTL). Combina libremente cuantificadores de ruta y operadores temporales. Al igual que CTL, CTL* es una lógica de tiempo ramificado. La semántica formal de las fórmulas de CTL* se define con respecto a una estructura de Kripke dada .

Historia

LTL se propuso para la verificación de programas informáticos, por primera vez por Amir Pnueli en 1977. Cuatro años después, en 1981, EM Clarke y EA Emerson inventaron CTL y la verificación de modelos CTL . CTL* fue definido por EA Emerson y Joseph Y. Halpern en 1983. ^{[ 1 ]}

CTL y LTL se desarrollaron de forma independiente antes que CTL*. Ambas sublógicas se han convertido en estándares en la comunidad de verificación de modelos , mientras que CTL* tiene importancia práctica porque proporciona un banco de pruebas expresivo para representar y comparar estas y otras lógicas. Esto es sorprendente porque la complejidad computacional de la verificación de modelos en CTL* no es peor que la de LTL: ambas se encuentran en PSPACE .

Sintaxis

El lenguaje de las fórmulas CTL* bien formadas se genera mediante la siguiente gramática libre de contexto no ambigua (con respecto al uso de corchetes) :

{\displaystyle \Phi

{\displaystyle \phi

dónde $p$ abarca un conjunto de fórmulas atómicas . Las fórmulas CTL* válidas se construyen utilizando el no terminal. $\Phi$ Estas fórmulas se denominan fórmulas de estado , mientras que las creadas por el símbolo $\phi$ se denominan fórmulas de ruta . (La gramática anterior contiene algunas redundancias; por ejemplo $\Phi \lor \Phi$ así como la implicación y la equivalencia pueden definirse simplemente para las álgebras booleanas (o lógica proposicional ) a partir de la negación y la conjunción, y los operadores temporales X y U son suficientes para definir las otras dos .

Los operadores son básicamente los mismos que en CTL . Sin embargo, en CTL, cada operador temporal ( $X,F,G,U$ ) debe ir precedido directamente por un cuantificador, mientras que en CTL* esto no es necesario. El cuantificador de ruta universal puede definirse en CTL* de la misma manera que para el cálculo de predicados clásico. $A\phi =\neg E\neg \phi$ , aunque esto no es posible en el fragmento CTL.

Ejemplos de fórmulas

Fórmula CTL* que no está ni en LTL ni en CTL: $EX(p)\land AFG(p)$
Fórmula LTL que no está en CTL: $\ AFG(p)$
Fórmula CTL que no está en LTL: $\ EX(p)$
Fórmula CTL* que se encuentra en CTL y LTL: $\ AG(p)$

Nota: Cuando se toma LTL como subconjunto de CTL*, cualquier fórmula LTL se antepone implícitamente con el cuantificador de ruta universal. $A$ .

Semántica

La semántica de CTL* se define con respecto a alguna estructura de Kripke . Como su nombre indica, las fórmulas de estado se interpretan con respecto a los estados de esta estructura, mientras que las fórmulas de ruta se interpretan sobre las rutas que la componen.

Fórmulas de estado

Si un estado $s$ de la estructura de Kripke satisface una fórmula de estado $\Phi$ se denota $s\modelos \Phi$ Esta relación se define inductivamente de la siguiente manera:

${\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
${\Big (}({\mathcal {M}},s)\models \neg \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}$
${\Big (}({\mathcal {M}},s)\models \Phi _{1}\land \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models \Phi _{1}\lor \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models \Phi _{1}\Rightarrow \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}$
${\bigg (}({\mathcal {M}},s)\models \Phi _{1}\Leftrightarrow \Phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}{\bigg )}$
${\Big (}({\mathcal {M}},s)\models A\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ para todos los caminos $\ \pi$ comenzando en $s{\Big )}$
${\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ por algún camino $\ \pi$ comenzando en $s{\Big )}$

Fórmulas de ruta

La relación de satisfacción $\pi \models \phi$ para fórmulas de ruta $\ \phi$ y un camino $\pi =s_{0}\to s_{1}\to \cdots$ También se define inductivamente. Para ello, sea $\ \pi [n]$ denota la subruta $s_{n}\to s_{n+1}\to \cdots$ :

${\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s_{0})\models \Phi {\Big )}$
${\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\Big )}$
${\Big (}\pi \models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\Big (}\pi \models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\Big (}\pi \models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}\pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}$
${\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \phi {\Big )}$
${\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \phi _{2}\land \forall 0\leqslant k<n:~\pi [k]\models \phi _{1}{\big )}{\Big )}$

Problemas de decisión

La verificación de modelos CTL* (de una fórmula de entrada en un modelo fijo) es PSPACE-completa ^{[ 2 ]} y el problema de satisfacibilidad es 2EXPTIME -completa. ^{[ 2 ]}^{[ 3 ]}

Véase también

Referencias

^ Emerson, E. Allen; Halpern, Joseph Y. (1983). ""A veces" y "Nunca" revisitados". Actas del 10.º Simposio ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación - POPL '83 . págs. 127-140 . doi : 10.1145/567067.567081 . ISBN 0897910907. S2CID 15728260 .
1 2 Baier, Christel ; Katoen, Joost-Pieter (1 de enero de 2008). Principios de verificación de modelos (serie Representación y Mente) . La prensa del MIT. ISBN 978-0262026499.
↑ Orna Kupferman ; Moshe Y. Vardi (junio de 1999). " El problema de Church revisitado". Boletín de lógica simbólica . 5 (2): 245– 263. doi : 10.2307/421091 . JSTOR 421091. S2CID 18833301 .

Amir Pnueli : La lógica temporal de los programas. Actas del 18.º Simposio Anual del IEEE sobre Fundamentos de la Informática (FOCS), 1977, 46-57. DOI= 10.1109/SFCS.1977.32
E. Allen Emerson , Joseph Y. Halpern : «A veces» y «nunca» revisitados: sobre la lógica temporal ramificada frente a la lineal. Journal of the ACM 33, 1 (enero de 1986), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
Ph. Schnoebelen: La complejidad de la verificación de modelos de lógica temporal. Avances en lógica modal 2002: 393–436

Enlaces externos

Diapositivas didácticas del profesor Alessandro Artale en la Universidad Libre de Bozen-Bolzano.

[EmersonHalpern1983-1] Emerson, E. Allen; Halpern, Joseph Y. (1983). ""A veces" y "Nunca" revisitados". Actas del 10.º Simposio ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación - POPL '83 . págs. 127-140 . doi : 10.1145/567067.567081 . ISBN 0897910907. S2CID 15728260 .

[:0-2] 1 2 Baier, Christel ; Katoen, Joost-Pieter (1 de enero de 2008). Principios de verificación de modelos (serie Representación y Mente) . La prensa del MIT. ISBN 978-0262026499.

[3] Orna Kupferman ; Moshe Y. Vardi (junio de 1999). " El problema de Church revisitado". Boletín de lógica simbólica . 5 (2): 245– 263. doi : 10.2307/421091 . JSTOR 421091. S2CID 18833301 .

[ 1 ]

[ 3 ]