Lógica del árbol de cálculo

La lógica de árbol de cómputo ( CTL ) es una lógica de tiempo ramificado , lo que significa que su modelo de tiempo es una estructura similar a un árbol en la que el futuro no está determinado; hay diferentes caminos en el futuro, cualquiera de los cuales podría ser un camino real que se realiza. Se utiliza en la verificación formal de artefactos de software o hardware, típicamente por aplicaciones de software conocidas como verificadores de modelos , que determinan si un artefacto dado posee propiedades de seguridad o vitalidad . Por ejemplo, CTL puede especificar que cuando se satisface alguna condición inicial (por ejemplo, todas las variables del programa son positivas o ningún automóvil en una autopista se extiende a ambos lados de dos carriles), entonces todas las posibles ejecuciones de un programa evitan alguna condición indeseable (por ejemplo, dividir un número por cero o dos automóviles chocando en una autopista). En este ejemplo, la propiedad de seguridad podría verificarse mediante un verificador de modelos que explora todas las posibles transiciones fuera de los estados del programa que satisfacen la condición inicial y garantiza que todas esas ejecuciones satisfacen la propiedad. La lógica de árbol de cómputo pertenece a una clase de lógicas temporales que incluye la lógica temporal lineal  (LTL). Aunque hay propiedades expresables solo en CTL y propiedades expresables solo en LTL, todas las propiedades expresables en cualquiera de las 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, ha habido un debate sobre los méritos relativos de CTL y LTL. Debido a que CTL es más eficiente computacionalmente 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 usan 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 :

${\displaystyle {\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{aligned}}}$

donde abarca un conjunto de fórmulas atómicas . No es necesario utilizar todos los conectivos; por ejemplo, comprende un conjunto completo de conectivos y los demás pueden definirse utilizándolos. ${\displaystyle p}$ ${\displaystyle \{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}}$

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

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

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

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

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

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

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

Operadores

Operadores lógicos

Los operadores lógicos son los habituales: ¬, ∨, ∧, ⇒ y ⇔. Junto con estos operadores, las fórmulas CTL también pueden hacer uso de las constantes booleanas true y false .

Operadores temporales

Los operadores temporales son los siguientes:

• Cuantificadores sobre caminos
  • A Φ – A all: Φ debe cumplirse en todas las rutas a partir del estado actual.
  • E Φ – E xiste: existe al menos un camino que parte del estado actual donde Φ se cumple.
• Cuantificadores específicos de ruta
  • X φ  – Siguiente : φ debe cumplirse en el siguiente estado (este operador a veces se denota N en lugar de X ).
  • G φ  – Globalmente : φ debe mantenerse en todo el camino subsiguiente.
  • F φ  – F inalmente: φ eventualmente tiene que mantenerse (en algún lugar del camino subsiguiente).
  • φ U ψ  – Hasta que: φ tiene que 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. Vea los ejemplos a continuación. CTL* es estrictamente más expresivo que CTL.

Conjunto mínimo de operadores

En CTL hay conjuntos mínimos de operadores. Todas las fórmulas de CTL se pueden transformar para utilizar solo esos operadores. Esto resulta útil en la comprobació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 una tripleta , donde es un conjunto de estados, es una relación de transición, que se supone que es serial, es decir, cada estado tiene al menos un sucesor, y es una función de etiquetado, que asigna letras proposicionales a los estados. Sea un modelo de transición de este tipo, con , y , donde es el conjunto de fórmulas bien formadas sobre el lenguaje de . ${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}$ ${\displaystyle S}$ ${\displaystyle {\rightarrow }\subseteq S\times S}$ ${\displaystyle L}$ ${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$ ${\displaystyle s\in S}$ ${\displaystyle \phi \in F}$ ${\displaystyle F}$ ${\displaystyle {\mathcal {M}}}$

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

1. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
2. ${\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}$
3. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}}$
4. ${\displaystyle {\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 )}}$
5. ${\displaystyle {\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 )}}$
6. ${\displaystyle {\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 )}}$
7. ${\displaystyle {\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 )}}$
8. ${\displaystyle {\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 )}}$
9. ${\displaystyle {\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 )}}$
10. ${\displaystyle {\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 )}}$
11. ${\displaystyle {\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 )}}$
12. ${\displaystyle {\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 )}}$
13. ${\displaystyle {\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 )}}$
14. ${\displaystyle {\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 )}}$
15. ${\displaystyle {\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 CTL

Las reglas 10 a 15 anteriores se refieren a las rutas de cálculo en los modelos y son las que en última instancia caracterizan al "árbol de cálculo"; son afirmaciones sobre la naturaleza del árbol de cálculo infinitamente profundo cuya raíz está en el estado dado . ${\displaystyle s}$

Equivalencias semánticas

Se dice que las fórmulas y son semánticamente equivalentes si cualquier estado en cualquier modelo que satisface una también satisface la otra. Esto se denota ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi \equiv \psi }$

Se puede observar que y son duales, siendo cuantificadores de ruta de cálculo universal y existencial respectivamente: . ${\displaystyle \mathrm {A} }$ ${\displaystyle \mathrm {E} }$ ${\displaystyle \neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi }$

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

Por lo tanto, una instancia de las leyes de De Morgan se puede formular en CTL:

${\displaystyle \neg AF\phi \equiv EG\neg \phi }$

${\displaystyle \neg EF\phi \equiv AG\neg \phi }$

${\displaystyle \neg AX\phi \equiv EX\neg \phi }$

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

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

${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$

${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$

${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$

${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$

Ejemplos

Sea "P" "me gusta el chocolate" y Q "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.P.​​​

"Siempre es posible (AF) que de repente empiece a gustarme el chocolate por el resto de mi vida". (Nota: no sólo por el resto de mi vida, ya que mi vida es finita, mientras que G es infinito).

• Por ejemplo , AF.P.

"Dependiendo de lo que pase en el futuro (E), es posible que durante el resto de mi vida (G), tenga garantizado al menos un día (AF) en el que me guste el chocolate. Sin embargo, si algo sale mal, entonces no hay ninguna garantía de que algún día me guste el chocolate".

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

• AG (P U Q)

"Desde ahora hasta que haga calor afuera, me gustará el chocolate todos los días. Una vez que haga calor afuera, no habrá ninguna duda de si me gustará el chocolate o no. Ah, y está garantizado que eventualmente hará calor afuera, aunque sea solo por un día".

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

"Es posible que: eventualmente llegará un momento en que hará calor para siempre (AG.Q) y que antes de ese momento siempre habrá alguna manera de lograr que me guste el chocolate al día siguiente (EX.P)".

Relaciones con otras lógicas

La lógica de árbol computacional (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 de cálculo (CTL) y la lógica temporal lineal (LTL) son ambas un subconjunto de CTL*. CTL y LTL no son equivalentes y tienen un subconjunto común, que es un subconjunto propio de CTL y 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

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

• La semántica del árbol. Etiquetamos los nodos del árbol de cálculo. QCTL* = QCTL = MSO sobre árboles. La verificación y la satisfacibilidad del modelo son completamente completas.
• La semántica de la estructura. Etiquetamos los estados. QCTL* = QCTL = MSO sobre grafos . La comprobación del modelo es PSPACE-completa pero la satisfacibilidad es indecidible .

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

Véase también

• CTL probabilístico
• Lógica de árbol computacional justa
• Lógica temporal lineal

Referencias

1. Vardi, Moshe Y. (2001). "Ramificación vs. Tiempo lineal: enfrentamiento final" (PDF) . Apuntes de clase en informática. Vol. 2031. Springer, Berlín. págs. 1–22. doi :10.1007/3-540-45319-9_1. ISBN 978-3-540-41865-8. {{cite book}}: |journal=ignorado ( ayuda ) ; faltante o vacío |title=( ayuda )
2. David, Amélie; Laroussinie, Francois; Markey, Nicolas (2016). Desharnais, Josée; Jagadeesan, Radha (eds.). "Sobre la expresividad de QCTL". 27.ª Conferencia internacional sobre teoría de la concurrencia (CONCUR 2016) . Leibniz International Proceedings in Informatics (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.). "De CTL cuantificado a QBF". 26.º Simposio internacional sobre representación y razonamiento temporal (TIME 2019) . Leibniz International Proceedings in Informatics (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 utilizando lógica temporal de ramificación" (PDF) . Lógica de programas, Actas del taller, Notas de clase en informática . Vol. 131. Springer, Berlín. págs. 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". Revista de Ciencias de la Computación y de Sistemas . 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 utilizando 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.). Handbook of Theoretical Computer Science, vol. B. MIT Press. págs. 955–1072. ISBN 978-0-262-22039-2.

Enlaces externos

• Diapositivas didácticas de CTL