La lógica de árbol de cálculo ( CTL ) es una lógica de tiempo de ramificación , lo que significa que su modelo de tiempo es una estructura en forma de á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, generalmente mediante aplicaciones de software conocidas como verificadores de modelos , que determinan si un artefacto determinado posee seguridad o vitalidad.propiedades. Por ejemplo, CTL puede especificar que cuando se satisface alguna condición inicial (p. Ej., Todas las variables del programa son positivas o ningún automóvil en una carretera cruza dos carriles), entonces todas las ejecuciones posibles de un programa evitan alguna condición no deseada (p. Ej., Dividir un número entre cero o dos coches chocando en una carretera). En este ejemplo, la propiedad de seguridad podría ser verificada por un verificador de modelos que explora todas las posibles transiciones fuera de los estados del programa que satisfacen la condición inicial y asegura que todas estas ejecuciones satisfacen la propiedad. La lógica del árbol de cálculo pertenece a una clase de lógica temporal que incluye la lógica temporal lineal (LTL). Aunque hay propiedades que se pueden expresar solo en CTL y propiedades que se pueden expresar solo en LTL, todas las propiedades que se pueden expresar en cualquier lógica también se pueden expresar en CTL * .
CTL fue propuesto por primera vez por Edmund M. Clarke y E. Allen Emerson en 1981, quienes lo usaron para sintetizar los llamados esqueletos de sincronización , es decir , abstracciones de programas concurrentes .
Sintaxis de CTL
El lenguaje de fórmulas bien formadas para CTL se genera mediante la siguiente gramática :
dónde rangos sobre un conjunto de fórmulas atómicas . No es necesario utilizar todos los conectores, por ejemplo, comprende un conjunto completo de conectivos, y los demás se pueden definir con ellos.
- significa 'por todos los caminos' (inevitablemente)
- significa 'a lo largo de al menos (existe) un camino' (posiblemente)
Por ejemplo, la siguiente es una fórmula CTL bien formada:
- )
La siguiente no es una fórmula CTL bien formada:
El problema con esta cadena es que puede ocurrir solo cuando se combina con un o un .
CTL usa proposiciones atómicas como sus bloques de construcción para hacer declaraciones sobre los estados de un sistema. Estas proposiciones luego se combinan en fórmulas utilizando operadores lógicos y operadores temporales .
Operadores
Operadores logicos
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 verdadero y falso .
Operadores temporales
Los operadores temporales son los siguientes:
- Cuantificadores sobre caminos
- A Φ - A ll: Φ debe mantenerse en todas las rutas a partir del estado actual.
- E Φ - E xistas: existe al menos una ruta a partir del estado actual donde Φ se mantiene.
- Cuantificadores de ruta específica
- X φ - Ne x t: φ debe mantenerse en el siguiente estado (este operador a veces se indica como N en lugar de X ).
- G φ - G lobally: φ debe mantenerse en toda la ruta posterior.
- F φ - F inally: φ eventualmente tiene que aguantar (en algún lugar de la ruta siguiente).
- φ U ψ - U ntil: φ debe mantenerse al menos hasta que en alguna posición ψ se mantenga. Esto implica que ψ se verificará en el futuro.
- φ W ψ - W EAK hasta que: φ tiene que sostener hasta ψ bodegas. La diferencia con U es que no hay garantía de que ψ alguna vez se verifique. El operador W a veces se llama "a menos que".
En CTL * , los operadores temporales se pueden mezclar libremente. En CTL, el operador siempre debe estar agrupado en dos: un operador de ruta seguido por un operador estatal. 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 CTL se pueden transformar para usar solo esos operadores. Esto es útil en la verificación de modelos . Un conjunto mínimo de operadores es: {verdadero, ∨, ¬, 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 el sistema de transición . Un sistema de transición es un triple, dónde es un conjunto de estados, es una relación de transición, asumida como serial, es decir, cada estado tiene al menos un sucesor, y es una función de etiquetado, que asigna letras proposicionales a los estados. Dejar ser un modelo de transición
Entonces la relación de vinculación semántica se define de forma recursiva en :
Caracterización de CTL
Las reglas 10-15 anteriores se refieren a rutas de cálculo en modelos y son las que caracterizan en última instancia al "árbol de cálculo"; son afirmaciones sobre la naturaleza del árbol de cálculo infinitamente profundo enraizado en el estado dado.
Equivalencias semánticas
Las fórmulas y Se dice que son semánticamente equivalentes si cualquier estado en cualquier modelo que satisfaga a uno también satisface al otro. Esto se denota
Se puede ver que A y E son duales, siendo cuantificadores de ruta de cálculo universal y existencial respectivamente: .
Además, también lo son G y F.
Por lo tanto , se puede formular una instancia de las leyes de De Morgan en CTL:
Se puede demostrar usando tales 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.
Las equivalencias importantes a continuación se denominan leyes de expansión ; permiten desplegar la verificación de un conectivo CTL hacia sus sucesores en el tiempo.
Ejemplos de
Deje que "P" signifique "Me gusta el chocolate" y Q signifique "Hace calor afuera".
- AG .P
- "Me gustará el chocolate a partir de ahora, 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 por el resto del tiempo". (Nota: no solo el resto de mi vida, ya que mi vida es finita, mientras que G es infinita).
- EG . 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) que me guste el chocolate todavía por delante. Sin embargo, si algo sale mal , entonces todas las apuestas están canceladas y no hay garantía de si alguna vez me gustará el chocolate ".
Los dos ejemplos siguientes muestran la diferencia entre CTL y CTL *, ya que permiten que el operador hasta no esté calificado 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, todas las apuestas están canceladas en cuanto a si me gustará más el chocolate. Ah, y está garantizado que eventualmente hará calor afuera, aunque solo sea por un solo día ".
- EF (( EX. P) U ( AG .Q))
- "Es posible que: eventualmente llegue un momento en que hará calor para siempre (AG.Q) y que antes de ese momento siempre habrá alguna forma de hacer que me guste el chocolate al día siguiente (EX.P)".
Relaciones con otras lógicas
La lógica del árbol de cálculo (CTL) es un subconjunto de CTL *, así como del cálculo μ modal . CTL es también 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 un subconjunto de CTL *. CTL y LTL no son equivalentes y tienen un subconjunto común, que es un subconjunto adecuado 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
CTL se ha ampliado con cuantificación de segundo orden y a la lógica de árbol computacional cuantificada (QCTL). [1] Hay dos semánticas:
- la semántica del árbol. Etiquetamos los nodos del árbol de cálculo. QCTL * = QCTL = MSO sobre árboles. La verificación y la satisfacción del modelo están completas.
- la semántica de la estructura. Etiquetamos estados. QCTL * = QCTL = MSO sobre gráficos . La verificación del modelo es completa con PSPACE, pero la satisfacción es indecidible .
Se ha propuesto una reducción del problema de verificación de modelos de QCTL con la semántica de la estructura, a TQBF (fórmulas booleanas cuantificadas verdaderas), con el fin de aprovechar los solucionadores de QBF. [2]
Ver también
Referencias
- ^ David, Amélie; Laroussinie, Francois; Markey, Nicolas (2016). Desharnais, Josée; Jagadeesan, Radha (eds.). "Sobre la expresividad de QCTL" . XXVII Congreso Internacional de Teoría de la Concurrencia (CONCUR 2016) . Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik. 59 : 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.). "De CTL cuantificado a QBF" . XXVI Simposio Internacional de Representación Temporal y Razonamiento (TIME 2019) . Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik. 147 : 11: 1–11: 20. doi : 10.4230 / LIPIcs.TIME.2019.11 . ISBN 978-3-95977-127-6.
- EM Clarke; EA Emerson (1981). "Diseño y síntesis de esqueletos de sincronización mediante lógica temporal de tiempo de ramificación" (PDF) . Lógica de Programas, Actas de Taller, Notas de Conferencia en Ciencias de la Computación . Springer, Berlín. 131 : 52–71.
- Michael Huth; Mark Ryan (2004). Lógica en Ciencias de la Computación (Segunda Edición) . Prensa de la Universidad de Cambridge. pag. 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 de ramificación". Revista de Ciencias de la Computación y Sistemas . 30 (1): 1–24. doi : 10.1016 / 0022-0000 (85) 90001-7 .
- Clarke, EM; Emerson, EA y Sistla, AP (1986). "Verificación automática de sistemas concurrentes de estado finito utilizando especificaciones lógicas temporales". Transacciones ACM sobre lenguajes y sistemas de programación . 8 (2): 244–263. doi : 10.1145 / 5397.5399 .
- Emerson, EA (1990). "Lógica temporal y modal". En Jan van Leeuwen (ed.). Manual de Informática Teórica, vol. B . Prensa del MIT. págs. 955-1072. ISBN 978-0-262-22039-2.
enlaces externos
- Diapositivas didácticas de CTL