En la verificación formal , la verificación del modelo de estados finitos necesita encontrar un autómata Büchi (BA) equivalente a una fórmula de lógica temporal lineal (LTL) dada , es decir, tal que la fórmula LTL y BA reconozcan el mismo lenguaje ω . Hay algoritmos que traducen una fórmula LTL en un BA. [1] [2] [3] [4] Esta transformación se realiza normalmente en dos pasos. El primer paso produce un autómata Büchi generalizado (GBA) a partir de una fórmula LTL. El segundo paso traduce este GBA en un BA, lo que implica una construcción relativamente fácil.. Dado que LTL es estrictamente menos expresivo que BA, la construcción inversa no siempre es posible.
Los algoritmos para transformar LTL en GBA difieren en sus estrategias de construcción, pero todos tienen un principio subyacente común, es decir, cada estado en el autómata construido representa un conjunto de fórmulas LTL que se espera sean satisfechas por la palabra de entrada restante después de la ocurrencia del estado. durante una carrera.
Transformación de LTL a GBA
Aquí se presentan dos algoritmos para la construcción. El primero proporciona una construcción declarativa y fácil de entender. El segundo proporciona una construcción algorítmica y eficiente. Ambos algoritmos asumen que la fórmula de entrada f se construye usando el conjunto de variables proposicionales AP yf está en forma normal de negación . Para cada fórmula LTL f 'sin ¬ como símbolo superior, sea neg (f') = ¬f ', neg (¬f') = f '. Para un caso especial f '= verdadero , sea neg ( verdadero ) = falso .
Construcción declarativa
Antes de describir la construcción, necesitamos presentar algunas definiciones auxiliares. Para una fórmula LTL f , sea cl (f) el conjunto más pequeño de fórmulas que satisfaga las siguientes condiciones:
|
|
cl (f) es el cierre de sub-fórmulas de f bajo negación. Tenga en cuenta que cl (f) puede contener fórmulas que no están en forma normal de negación. Los subconjuntos de cl (f) servirán como estados del GBA equivalente. Nuestro objetivo es construir el GBA de manera que si un estado corresponde a un subconjunto M ⊂ cl (f), entonces el GBA tiene una ejecución de aceptación comenzando desde el estado de una palabra si si la palabra satisface todas las fórmulas en M y viola todas las fórmulas en cl ( f) / M. Por esta razón, no consideraremos cada conjunto de fórmulas M que sea claramente inconsistente o subsumido por un superconjunto estrictamente M 'tal que M y M' sean equiv-satisfactorios. Un conjunto M ⊂ cl (f) es máximamente consistente si satisface las siguientes condiciones:
|
|
Sea cs (f) el conjunto de subconjuntos máximamente consistentes de cl (f). Usaremos solo cs (f) como los estados de GBA.
- Construcción GBA
Un GBA equivalente af es A = ({init} ∪ cs (f), 2 AP , Δ, {init}, F ), donde
- Δ = Δ 1 ∪ Δ 2
- (M, a, M ') ∈ Δ 1 sif (M' ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M '} y:
- X f 1 ∈ M si f f 1 ∈ M ';
- f 1 U f 2 ∈ M si f 2 ∈ M o (f 1 ∈ M yf 1 U f 2 ∈ M ');
- f 1 R f 2 ∈ M si f f 1 ∧ f 2 ∈ M o (f 2 ∈ M yf 1 R f 2 ∈ M ')
- Δ 2 = {(init, a, M ') | (M '∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M '} yf ∈ M'}
- (M, a, M ') ∈ Δ 1 sif (M' ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M '} y:
- Para cada f 1 U f 2 ∈ cl (f), {M ∈ cs (f) | f 2 ∈ M o ¬ (f 1 U f 2 ) ∈ M} ∈ F
Las tres condiciones en la definición de Δ 1 aseguran que cualquier ejecución de A no viole la semántica de los operadores temporales. Tenga en cuenta que F es un conjunto de conjuntos de estados. Los conjuntos en F se definen para capturar una propiedad del operador U que no se puede verificar comparando dos estados consecutivos en una carrera, es decir, si f 1 U f 2 es verdadera en algún estado, finalmente f 2 es verdadera en algún estado posterior .
Sea-palabra w = a 1 , a 2 , ... sobre el alfabeto 2 AP . Sea w i = a i , a i + 1 , .... Sea M w = {f '∈ cl (f) | w f '}, que llamamos conjunto satisfactorio . Debido a la definición de cs (f), M w ∈ cs (f). Podemos definir una secuencia ρ w = init, M w 1 , M w 2 , .... Debido a la definición de A , si wf entonces ρ w debe ser una corrida aceptable de A sobre w .
A la inversa, supongamos que A acepta w . Sea ρ = init, M 1 , M 2 , ... una corrida de A sobre w . El siguiente teorema completa el resto de la prueba de corrección.
Teorema 1: Para todo i> 0, M w i = M i .
Prueba: La prueba es por inducción sobre la estructura de f '∈ cl (f).
- Casos base:
- f '= verdadero . Por definiciones, f '∈ M w i y f' ∈ M i .
- f '= p. Por definición de A , p ∈ M i iff p ∈ a i iff p ∈ M w i .
- Pasos de inducción:
- f '= f 1 ∧ f 2 . Debido a la definición de conjuntos consistentes, f 1 ∧ f 2 ∈ M i iff f 1 ∈ M i y f 2 ∈ M i . Debido a la hipótesis de inducción, f 1 ∈ M w i y f 2 ∈ M w i . Debido a la definición de conjunto satisfactorio, f 1 ∧ f 2 ∈ M w i .
- f '= ¬f 1 , f' = f 1 ∨ f 2 , f '= X f 1 o f' = f 1 R f 2 . Las pruebas son muy similares a la anterior.
- f '= f 1 U f 2 . La prueba de igualdad se divide en dos pruebas de vinculación.
- Si f 1 U f 2 ∈ M i , entonces f 1 U f 2 ∈ M w i . Por la definición de las transiciones de A , podemos tener los siguientes dos casos.
- f 2 ∈ M i . Por hipótesis de inducción, f 2 ∈ M w i . Entonces, f 1 U f 2 ∈ M w i .
- f 1 ∈ M i y f 1 U f 2 ∈ M i + 1 . Y debido a la condición de aceptación de A , hay al menos un índice j ≥ i tal que f 2 ∈ M j . Sea j 'el más pequeño de estos índices. Demostramos el resultado por inducción en k = {j ', j'-1, ..., i + 1, i}. Si k = j ', entonces f 2 ∈ M k , aplicamos el mismo argumento que en el caso de f 2 ∈ M i . Si i ≤ k
2 ∉ M k , y entonces f 1 ∈ M k y f 1 U f 2 ∈ M k + 1 . Debido a la hipótesis de inducción en f ', tenemos f 1 ∈ M w k . Debido a la hipótesis de inducción sobre índices, también tenemos f 1 U f 2 ∈ M w k + 1 . Debido a la definición de la semántica de LTL, f 1 U f 2 ∈ M w k .
- Si f 1 U f 2 ∈ M w i , entonces f 1 U f 2 ∈ M i . Debido a la semántica de LTL, podemos tener los siguientes dos casos.
- f 2 ∈ M w i . Por hipótesis de inducción, f 2 ∈ M i . Entonces, f 1 U f 2 ∈ M i .
- f 1 ∈ M w i yf 1 U f 2 ∈ M w i + 1 . Debido a la semántica LTL, hay al menos un índice j ≥ i tal que f 2 ∈ M j . Sea j 'el más pequeño de estos índices. Proceda ahora como prueba de la implicación inversa.
- Si f 1 U f 2 ∈ M i , entonces f 1 U f 2 ∈ M w i . Por la definición de las transiciones de A , podemos tener los siguientes dos casos.
Debido al teorema anterior, M w 1 = M 1 . Debido a la definición de las transiciones de A , f ∈ M 1 . Por tanto, f ∈ M w 1 y w F.
Gerth y col. algoritmo
El siguiente algoritmo se debe a Gerth, Peled, Vardi y Wolper . [3] También está disponible un mecanismo de construcción verificado de esto por Schimpf, Merz y Smaus. [5] La construcción anterior crea exponencialmente muchos estados por adelantado y muchos de esos estados pueden ser inalcanzables. El siguiente algoritmo evita esta construcción inicial y tiene dos pasos. En el primer paso, construye de forma incremental un gráfico dirigido. En el segundo paso, construye un autómata Büchi generalizado etiquetado (LGBA) definiendo los nodos del gráfico como estados y los bordes dirigidos como transiciones. Este algoritmo tiene en cuenta la accesibilidad y puede producir un autómata más pequeño, pero la complejidad del peor de los casos sigue siendo la misma.
Los nodos del gráfico están etiquetados por conjuntos de fórmulas y se obtienen descomponiendo fórmulas de acuerdo con su estructura booleana, y expandiendo los operadores temporales para separar lo que tiene que ser verdad inmediatamente de lo que tiene que ser verdad a partir del siguiente estado. . Por ejemplo, supongamos que aparece una fórmula LTL f 1 U f 2 en la etiqueta de un nodo. f 1 U f 2 es equivalente af 2 ∨ (f 1 ∧ X (f 1 U f 2 )). La expansión equivalente sugiere que f 1 U f 2 es verdadera en una de las dos condiciones siguientes.
- f 1 se mantiene en el momento actual y (f 1 U f 2 ) se mantiene en el siguiente paso de tiempo, o
- f 2 se mantiene en el intervalo de tiempo actual
Los dos casos se pueden codificar creando dos estados (nodos) del autómata y el autómata puede saltar de forma no determinista a cualquiera de ellos. En el primer caso, hemos descargado una parte de la carga de la prueba en el siguiente paso de tiempo, por lo tanto, también creamos otro estado (nodo) que llevará la obligación para el próximo paso de tiempo en su etiqueta.
También debemos considerar el operador temporal R que puede causar tal división de casos. f 1 R f 2 es equivalente a (f 1 ∧ f 2 ) ∨ (f 2 ∧ X (f 1 R f 2 )) y esta expansión equivalente sugiere que f 1 R f 2 es verdadera en una de las dos condiciones siguientes.
- f 2 se mantiene en el momento actual y (f 1 R f 2 ) se mantiene en el siguiente paso de tiempo, o
- (f 1 ∧ f 2 ) se mantiene en el intervalo de tiempo actual.
Para evitar muchos casos en el siguiente algoritmo, definamos las funciones curr1 , next1 y curr2 que codifican las equivalencias anteriores en la siguiente tabla.
F | curr1 (f) | siguiente1 (f) | curr2 (f) |
---|---|---|---|
f 1 U f 2 | {f 1 } | {f 1 U f 2 } | {f 2 } |
f 1 R f 2 | {f 2 } | {f 1 R f 2 } | {f 1 , f 2 } |
f 1 ∨ f 2 | {f 2 } | ∅ | {f 1 } |
También hemos agregado el caso de disyunción en la tabla anterior, ya que también causa una división de casos en el autómata.
Los siguientes son los dos pasos del algoritmo.
- Paso 1. create_graph
En el siguiente cuadro, presentamos la primera parte del algoritmo que construye un gráfico dirigido. create_graph es la función de entrada, que espera la fórmula de entrada f en la forma normal de negación . Llama a la función recursiva expandir que construye el gráfico llenando variables globales Nodes , Incoming , Now y Next . El conjunto de nodos almacena el conjunto de nodos en el gráfico. El mapa Incoming asigna cada nodo de Nodos a un subconjunto de Nodos ∪ {init}, que define el conjunto de bordes entrantes. La entrada de un nodo también puede contener un símbolo especial init que se usa en la construcción final del autómata para decidir el conjunto de estados iniciales. Ahora y Siguiente asignan cada nodo de nodos a un conjunto de fórmulas LTL. Para un nodo q, Now (q) denota el conjunto de fórmulas que deben ser satisfechas por el resto de la palabra de entrada si el autómata está actualmente en el nodo (estado) q. Siguiente (q) denota el conjunto de fórmulas que deben ser satisfechas por el resto de la palabra de entrada si el autómata se encuentra actualmente en el siguiente nodo (estado) después de q.
typedefs LTL : fórmulas LTL LTLSet : conjuntos de fórmulas LTL NodeSet : conjuntos de nodos de gráficos ∪ {init} globals Nodos : conjunto de nodos de gráfico: = ∅ Entrante : Nodos → NodeSet : = ∅ Ahora : Nodos → LTLSet : = ∅ Siguiente : Nodos → LTLSet : = ∅ función create_graph ( LTL f) { expandir ({f}, ∅, ∅, {init}) return ( Nodos , Ahora , Entrante ) }
función expandir ( LTLSet curr, LTLSet antiguo, LTLSet siguiente, NodeSet entrante) { 1: si curr = ∅ entonces 2: si ∃q ∈ Nodos : Siguiente (q) = siguiente ∧ Ahora (q) = antiguo entonces 3: Entrante (q): = Entrante (q) ∪ entrante 4: más 5: q: = nuevo_nodo () 6: Nodos : = Nodos ∪ {q} 7: Entrante (q): = entrante 8: Ahora (q): = antiguo 9: Siguiente (q): = siguiente10: expandir ( Siguiente (q), ∅, ∅, {q})11: más12: f ∈ curr13: curr: = curr \ {f}14: antiguo: = antiguo ∪ {f}15: haga coincidir f con 16: | verdadero , falso , p o ¬p, donde p ∈ AP →17: si f = falso ∨ neg (f) ∈ antiguo entonces 18: saltar 19: si no20: expandir (curr, antiguo, siguiente, entrante)21: | f 1 ∧ f 2 →22: expandir (curr ∪ ({f 1 , f 2 } \ antiguo), antiguo, siguiente, entrante)23: | X g →24: expandir (curr, antiguo, siguiente ∪ {g}, entrante) 25: | f 1 ∨ f 2 , f 1 U f 2 , of 1 R f 2 →26: expandir (curr ∪ ( curr1 (f) \ antiguo), antiguo, siguiente ∪ siguiente1 (f), entrante)27: expandir (curr ∪ ( curr2 (f) \ antiguo), antiguo, siguiente, entrante)28: regreso }
El código de expansión está etiquetado con números de línea para facilitar la referencia. Cada llamado a expandir tiene como objetivo agregar un nodo y sus nodos sucesores en el gráfico. Los parámetros de la llamada describen un posible nuevo nodo.
- El primer parámetro curr contiene el conjunto de fórmulas que aún no se han ampliado.
- El segundo parámetro antiguo contiene el conjunto de fórmulas que ya están expandidas.
- El tercer parámetro siguiente es el conjunto de la fórmula con el que se creará el nodo sucesor.
- El cuarto parámetro entrantes define un conjunto de bordes entrantes cuando el nodo se agrega al gráfico.
En la línea 1, la condición if verifica si curr contiene alguna fórmula para expandir. Si el curr está vacío, en la línea 2, la condición if verifica si ya existe un estado q 'con el mismo conjunto de fórmulas expandidas. Si ese es el caso, entonces no agregamos un nodo redundante, pero agregamos el parámetro entrante en Entrante (q ') en la línea 3. De lo contrario, agregamos un nuevo nodo q usando los parámetros en las líneas 5-9 y comenzamos a expandir un nodo sucesor de q usando next (q) como su conjunto no expandido de fórmulas en la línea 10.
En el caso de que curr no esté vacío, entonces tenemos más fórmulas para expandir y controlar los saltos de la línea 1 a la 12. En las líneas 12-14, se selecciona una fórmula f de curr y se mueve a la anterior . Dependiendo de la estructura de f, se ejecuta el resto de la función.
- Si f es un literal, entonces la expansión continúa en la línea 20, pero si old ya contiene neg (f) of = false , entonces old contiene una fórmula inconsistente y descartamos este nodo al no hacer ningún recursivo all en la línea 18.
- Si f = f 1 ∧ f 2 , entonces f 1 y f 2 se suman a curr y se realiza una llamada recursiva para una mayor expansión en la línea 22.
- Si f = X f 1 , entonces f 1 se suma al siguiente para el sucesor del nodo actual en consideración en la línea 24.
- Si f = f 1 ∨ f 2 , f = f 1 U f 2 , o f = f 1 R f 2, entonces el nodo actual se divide en dos nodos y para cada nodo se realiza una llamada recursiva.
Para las llamadas recursivas, curr y next se modifican utilizando las funciones curr1 , next1 y curr2 que se definieron en la tabla anterior.
- Paso 2. Construcción LGBA
Sea ( Nodos , Ahora , Entrante ) = create_graph (f). Un LGBA equivalente af es A = ( Nodos , 2 AP , L , Δ, Q 0 , F ), donde
- L = {(q, a) | q ∈ Nodos y ( Ahora (q) ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ Ahora (q)}}
- Δ = {(q, q ') | q, q '∈ Nodos yq ∈ Entrante (q')}
- Q 0 = {q ∈ Nodos | init ∈ Entrante (q)}
- Para cada subfórmula g = g 1 U g 2 , sea F g = {q ∈ Nodes | g 2 ∈ Ahora (q) o g ∉ Ahora (q)}, luego F = {F g | g ∈ cl (f)}
Tenga en cuenta que las etiquetas de los nodos en la construcción algorítmica no contienen la negación de las subfórmulas de f. En la construcción declarativa, un nodo tiene el conjunto de fórmulas que se espera que sean verdaderas. La construcción algorítmica asegura la corrección sin la necesidad de que todas las fórmulas verdaderas estén presentes en una etiqueta de nodo.
Herramientas
- SPOT LTL2TGBA : traductor LTL2TGBA incluido en la biblioteca de comprobación de modelos orientados a objetos SPOT. Traductor en línea disponible.
- LTL2BA : traductor rápido de LTL a BA mediante autómatas alternos. Traductor en línea disponible.
- LTL3BA : una mejora actualizada de LTL2BA.
Referencias
- ^ MY Vardi y P. Wolper, Razonamiento sobre cálculos infinitos, Información y Computación, 115 (1994), 1-37.
- ^ Y. Kesten, Z. Manna, H. McGuire, A. Pnueli, Un algoritmo de decisión para lógica temporal proposicional completa, CAV'93, Elounda, Grecia, LNCS 697, Springer-Verlag, 97-109.
- ^ a b R. Gerth, D. Peled, MY Vardi y P. Wolper, "Verificación automática simple sobre la marcha de la lógica temporal lineal", Proc. IFIP / WG6.1 Symp. Protocolo de especificación, prueba y verificación (PSTV95), págs. 3-18, Varsovia, Polonia, Chapman & Hall, junio de 1995.
- ↑ P. Gastin y D. Oddoux, Fast LTL to Büchi automata translation, Decimotercera Conferencia sobre Verificación Asistida por Computadora (CAV ′01), número 2102 en LNCS, Springer-Verlag (2001), págs. 53–65.
- ^ A. Schimpf, S. Merz y JG. Smaus, "Construcción de Autómatas Bu¨chi para Verificación de Modelos LTL Verificada en Isabelle / HOL", Proc. Conferencia internacional sobre demostración de teoremas en lógicas de orden superior (TPHOLs 2009), págs. 424-439, Munich, Alemania, Springer, agosto de 2009.