Lógica de árbol de computación

La lógica de árbol de computación ( CTL ) es una lógica de tiempo ramificado , lo que significa que su modelo de tiempo es una estructura arbórea en la que el futuro no está determinado; existen diferentes caminos hacia el futuro, cualquiera de los cuales podría ser un camino real que se materialice. Se utiliza en la verificación formal de artefactos de software o hardware, generalmente mediante aplicaciones de software conocidas como verificadores de modelos , que determinan si un artefacto dado posee propiedades de seguridad o vivacidad . Por ejemplo, la CTL puede especificar que cuando se cumple una condición inicial (por ejemplo, todas las variables del programa son positivas o ningún coche en una autopista ocupa dos carriles), entonces todas las posibles ejecuciones de un programa evitan una condición indeseable (por ejemplo, dividir un número por cero o que dos coches colisionen en una autopista). En este ejemplo, la propiedad de seguridad podría verificarse mediante un verificador de modelos que explore todas las transiciones posibles desde estados del programa que satisfagan la condición inicial y garantice que todas dichas ejecuciones satisfagan la propiedad. La lógica de árbol de computación pertenece a una clase de lógicas temporales que incluye la lógica temporal lineal (LTL). Aunque existen propiedades que solo se pueden expresar en CTL y propiedades que solo se pueden expresar en LTL, todas las propiedades que se pueden expresar en cualquiera de las dos lógicas también se pueden expresar en CTL* .

Historia

CTL fue propuesto por primera vez por Edmund M. Clarke y E. Allen Emerson en 1981, quienes lo utilizaron para sintetizar los llamados esqueletos de sincronización , es decir, abstracciones de programas concurrentes .

Desde la introducción de CTL, se ha debatido sobre las ventajas relativas de CTL y LTL. Debido a que CTL es computacionalmente más eficiente para la verificación de modelos, se ha vuelto más común en el uso industrial, y muchas de las herramientas de verificación de modelos más exitosas utilizan CTL como lenguaje de especificación . ^{[ 1 ]}

Sintaxis de CTL

El lenguaje de fórmulas bien formadas para CTL se genera mediante la siguiente gramática :

{\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\\&\mid \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }}\phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}[\phi {\mbox{ U }}\phi ]\mid {\mbox{E }}[\phi {\mbox{ U }}\phi ]\end{alineado}}

dónde $p$ abarca un conjunto de fórmulas atómicas . No es necesario utilizar todos los conectores ; por ejemplo, $\{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}$ comprende un conjunto completo de conectores, y los demás pueden definirse a partir de ellos.

${\mbox{A}}$ significa 'a lo largo de todos los caminos' (inevitablemente)
${\mbox{E}}$ significa 'a lo largo de al menos (existe) un camino' (posiblemente)

Por ejemplo, la siguiente es una fórmula CTL bien formada:

{\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)

La siguiente no es una fórmula CTL bien formulada:

{\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}

El problema con esta cadena es que $\mathrm {U}$ puede ocurrir solo cuando se combina con un $\mathrm {A}$ o un $\mathrm {E}$ .

CTL utiliza proposiciones atómicas como bloques de construcción para formular afirmaciones sobre los estados de un sistema. Estas proposiciones se combinan posteriormente en fórmulas mediante operadores lógicos y operadores temporales .

Operadores

Operadores lógicos

Los operadores lógicos son los habituales: ¬, ∨ , ∧ , ⇒ y ⇔. Además de estos operadores, las fórmulas CTL también pueden utilizar las constantes booleanas verdadero y falso .

Operadores temporales

Los operadores temporales son los siguientes:

Cuantificadores sobre rutas
- A Φ – A ll: Φ debe mantenerse en todos los caminos que parten del estado actual.
- E Φ – E existe: existe al menos un camino que comienza desde el estado actual donde se cumple Φ .
Cuantificadores específicos de la ruta
- X φ – Ne x t: φ tiene que mantenerse en el siguiente estado (este operador a veces se denota con N en lugar de X ).
- G φ – G globalmente: φ tiene que mantenerse en todo el camino subsiguiente.
- F φ – Finalmente: φ eventualmente tiene que cumplirse (en algún punto del camino subsiguiente).
- φ U ψ – Hasta : φ debe cumplirse al menos hasta que en alguna posición ψ se cumpla. Esto implica que ψ se verificará en el futuro.
- φ W ψ – Débil hasta que: φ debe cumplirse hasta que ψ se cumpla. La diferencia con U es que no hay garantía de que ψ se verifique alguna vez. El operador W a veces se denomina "a menos que".

En CTL* , los operadores temporales se pueden combinar libremente. En CTL, los operadores siempre deben agruparse en pares: un operador de ruta seguido de un operador de estado. Véanse los ejemplos a continuación. CTL* es estrictamente más expresivo que CTL.

Conjunto mínimo de operadores

En CTL existen conjuntos mínimos de operadores. Todas las fórmulas de CTL pueden transformarse para usar solo esos operadores. Esto es útil en la verificación de modelos . Un conjunto mínimo de operadores es: {true, ∨ , ¬, EG , EU , EX }.

Algunas de las transformaciones utilizadas para los operadores temporales son:

EF φ == E [verdadero U ( φ )] (porque F φ == [verdadero U ( φ )] )
AX φ == ¬ EX (¬ φ )
AG φ == ¬ EF (¬ φ ) == ¬ E [verdadero U (¬ φ )]
AF φ == A [verdadero U φ ] == ¬ EG (¬ φ )
A [ φ U ψ ] == ¬( E [(¬ ψ ) U ¬( φ ∨ ψ )] ∨ EG (¬ ψ ) )

Semántica de CTL

Definición

Las fórmulas CTL se interpretan sobre sistemas de transición . Un sistema de transición es un sistema triple. ${\mathcal {M}}=(S,{\rightarrow },L)$ , dónde $S$ es un conjunto de estados, ${\rightarrow }\subseteq S\times S$ es una relación de transición, que se supone serial, es decir, cada estado tiene al menos un sucesor, y $L$ es una función de etiquetado, que asigna letras proposicionales a los estados. ${\mathcal {M}}=(S,\rightarrow ,L)$ ser un modelo de transición de este tipo, con $s\in S$ , y $\phi \in F$ , dónde $F$ es el conjunto de fórmulas bien formadas sobre el lenguaje de ${\mathcal {M}}$ .

Luego, la relación de implicación semántica $({\mathcal {M}},s\models \phi )$ se define recursivamente en $\phi$ :

${\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 AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
${\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
${\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$
${\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$

Caracterización de los CTL

Las reglas 10 a 15 anteriores se refieren a las rutas de computación en los modelos y son lo que en última instancia caracteriza al "Árbol de Computación"; son afirmaciones sobre la naturaleza del árbol de computación infinitamente profundo enraizado en el estado dado. $s$ .

Equivalencias semánticas

Las fórmulas $\phi$ y $\psi$ Se dice que son semánticamente equivalentes si cualquier estado en cualquier modelo que satisface uno también satisface el otro. Esto se denota $\phi \equiv \psi$

Se puede observar que $\mathrm {A}$ y $\mathrm {E}$ son duales, siendo cuantificadores de rutas de computación universales y existenciales respectivamente: $\neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi$ .

Además, también lo son. $\mathrm {G}$ y $\mathrm {F}$ .

Por lo tanto, un ejemplo de las leyes de De Morgan puede formularse en CTL:

\neg AF\phi \equiv EG\neg \phi

\neg EF\phi \equiv AG\neg \phi

\neg AX\phi \equiv EX\neg \phi

Se puede demostrar utilizando tales identidades que un subconjunto de los conectores temporales CTL es adecuado si contiene $EU$ , al menos uno de $\{AX,EX\}$ y al menos uno de $\{EG,AF,AU\}$ y los conectores booleanos.

Las equivalencias importantes que se muestran a continuación se denominan leyes de expansión ; permiten desplegar la verificación de un conector CTL hacia sus sucesores en el tiempo.

AG\phi \equiv \phi \land AXAG\phi

EG\phi \equiv \phi \land EXEG\phi

AF\phi \equiv \phi \lor AXAF\phi

EF\phi \equiv \phi \lor EXEF\phi

A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])

E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])

Ejemplos

Que "P" signifique "Me gusta el chocolate" y "Q" signifique "Hace calor afuera".

AG .P

"A partir de ahora me gustará el chocolate, pase lo que pase."

EF .P

"Es posible que algún día me guste el chocolate, al menos por un día."

AF . EG .P

"Siempre es posible (AF) que de repente me empiece a gustar el chocolate para siempre." (Nota: no solo para siempre, ya que mi vida es finita, mientras que G es infinito).

Ej . . AF .P

"Dependiendo de lo que suceda en el futuro (E), es posible que durante el resto del tiempo (G), tenga garantizado al menos un (AF) día en el que me guste el chocolate. Sin embargo, si algo sale mal, entonces todo puede pasar y no hay garantía de que alguna vez me guste el chocolate."

Los dos ejemplos siguientes muestran la diferencia entre CTL y CTL*, ya que permiten que el operador until no esté calificado con ningún operador de ruta ( A o E ):

AG (P U Q)

"Desde ahora hasta que haga calor, me gustará el chocolate todos los días. Cuando haga calor, ya no sé si me gustará o no. Ah, y seguro que hará calor tarde o temprano, aunque solo sea por un día."

EF (( EX .P) U ( AG .Q))

"Es posible que: llegue un momento en que haga calor para siempre (AG.Q) y que antes de ese momento siempre haya alguna manera de hacer que me guste el chocolate al día siguiente (EX.P)."

Relaciones con otras lógicas

La lógica de árbol de computación (CTL) es un subconjunto de CTL*, así como del cálculo modal μ . CTL también es un fragmento de la lógica temporal de tiempo alterno (ATL) de Alur, Henzinger y Kupferman .

La lógica de árbol computacional (CTL) y la lógica temporal lineal (LTL) son subconjuntos de CTL*. CTL y LTL no son equivalentes y comparten un subconjunto común, que a su vez es un subconjunto propio tanto de CTL como de LTL.

FG .P existe en LTL pero no en CTL.
AG (P⇒(( EX .Q) ∧ ( EX ¬Q))) y AG.EF .P existen en CTL pero no en LTL.

Extensiones

CTL se ha ampliado con cuantificación de segundo orden. $\exists p$ y $\forall p$ a la lógica de árbol computacional cuantificada (QCTL). ^{[ 2 ]} Hay dos semánticas:

la semántica del árbol. Etiquetamos los nodos del árbol de computación. QCTL* = QCTL = MSO sobre árboles. La verificación de modelos y la satisfacibilidad son completas en torre.
la semántica de la estructura. Etiquetamos estados. QCTL* = QCTL = MSO sobre grafos . La verificación de modelos es PSPACE-completa pero la satisfacibilidad es indecidible .

Se ha propuesto una reducción del problema de verificación de modelos de QCTL con semántica de estructura a TQBF (fórmulas booleanas cuantificadas verdaderas) para aprovechar los solucionadores QBF. ^{[ 3 ]}

Véase también

Referencias

↑ Vardi, Moshe Y. (2001). Branching vs. Linear Time: Final Showdown (PDF) . Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 2031. Springer, Berlín. pp. 1–22 . doi : 10.1007/3-540-45319-9_1 . ISBN 978-3-540-41865-8.
^ David, Amélie; Laroussinie, Francois; Markey, Nicolás (2016). Desharnais, Josée; Jagadeesan, Radha (eds.). "Sobre la expresividad de QCTL" . 27° Congreso Internacional sobre Teoría de la Concurrencia (CONCUR 2016) . Procedimientos internacionales de informática de Leibniz (LIPIcs). 59 . Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik: 28:1–28:15. doi : 10.4230/LIPIcs.CONCUR.2016.28 . ISBN 978-3-95977-017-0.
↑ Hossain, Akash; Laroussinie, François (2019). Gamper, Johann; Pinchinat, Sophie; Sciavicco, Guido (eds.). "From Quantified CTL to QBF" . 26.º Simposio Internacional sobre Representación y Razonamiento Temporal (TIME 2019) . Actas Internacionales Leibniz en Informática (LIPIcs). 147. Dagstuhl, Alemania: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 11:1–11:20. doi : 10.4230/LIPIcs.TIME.2019.11 . ISBN 978-3-95977-127-6. S2CID 195345645 .

EM Clarke; EA Emerson (1981). «Diseño y síntesis de esqueletos de sincronización mediante lógica temporal de tiempo ramificado» (PDF) . Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science . Vol. 131. Springer, Berlín. pp. 52–71 . doi : 10.1007/BFb0025774 . ISBN 3-540-11212-X.
Michael Huth; Mark Ryan (2004). Lógica en la informática (Segunda edición). Cambridge University Press. pág. 207. ISBN 978-0-521-54310-1.
Emerson, EA; Halpern, JY (1985). "Procedimientos de decisión y expresividad en la lógica temporal del tiempo ramificado". Journal of Computer and System Sciences . 30 (1): 1– 24. CiteSeerX 10.1.1.221.6187 . doi : 10.1016/0022-0000(85)90001-7 .
Clarke, EM; Emerson, EA y Sistla, AP (1986). "Verificación automática de sistemas concurrentes de estados finitos mediante especificaciones de lógica temporal" . ACM Transactions on Programming Languages and Systems . 8 (2): 244– 263. doi : 10.1145/5397.5399 . S2CID 52853200 .
Emerson, EA (1990). «Lógica temporal y modal». En Jan van Leeuwen (ed.). Manual de informática teórica, vol. B. MIT Press. pp. 955–1072 . ISBN 978-0-262-22039-2.

Enlaces externos

Diapositivas didácticas de CTL

[1] Vardi, Moshe Y. (2001). Branching vs. Linear Time: Final Showdown (PDF) . Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 2031. Springer, Berlín. pp. 1–22 . doi : 10.1007/3-540-45319-9_1 . ISBN 978-3-540-41865-8.

[2] David, Amélie; Laroussinie, Francois; Markey, Nicolás (2016). Desharnais, Josée; Jagadeesan, Radha (eds.). "Sobre la expresividad de QCTL" . 27° Congreso Internacional sobre Teoría de la Concurrencia (CONCUR 2016) . Procedimientos internacionales de informática de Leibniz (LIPIcs). 59 . Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik: 28:1–28:15. doi : 10.4230/LIPIcs.CONCUR.2016.28 . ISBN 978-3-95977-017-0.

[3] Hossain, Akash; Laroussinie, François (2019). Gamper, Johann; Pinchinat, Sophie; Sciavicco, Guido (eds.). "From Quantified CTL to QBF" . 26.º Simposio Internacional sobre Representación y Razonamiento Temporal (TIME 2019) . Actas Internacionales Leibniz en Informática (LIPIcs). 147. Dagstuhl, Alemania: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 11:1–11:20. doi : 10.4230/LIPIcs.TIME.2019.11 . ISBN 978-3-95977-127-6. S2CID 195345645 .

[ 1 ]

[ 2 ]

[ 3 ]