Estructura de Kripke (verificación de modelos)

Una estructura de Kripke es una variación del sistema de transición , propuesto originalmente por Saul Kripke [ ^{1 ] ,} utilizado en la verificación de modelos ^{[ 2 ]} para representar el comportamiento de un sistema. Consiste en un grafo cuyos nodos representan los estados alcanzables del sistema y cuyas aristas representan las transiciones de estado, junto con una función de etiquetado que asigna a cada nodo un conjunto de propiedades que se cumplen en el estado correspondiente. Las lógicas temporales se interpretan tradicionalmente en términos de estructuras de Kripke.

Sea AP un conjunto de proposiciones atómicas , es decir, expresiones con valores booleanos formadas a partir de variables, constantes y símbolos de predicado. Clarke et al. ^{[ 3 ]} definen una estructura de Kripke sobre AP como una cuádrupla M = ( S , I , R , L ) que consta de

• un conjunto finito de estados S .
• un conjunto de estados iniciales I ⊆ S .
• una relación de transición R ⊆ S × S tal que R es izquierda-total , es decir, ∀s ∈ S ∃s' ∈ S tal que (s,s') ∈ R .
• una función de etiquetado (o interpretación ) L : S → 2 ^AP .

Dado que R es totalmente izquierda , siempre es posible construir un camino infinito a través de la estructura de Kripke. Un estado de interbloqueo puede modelarse mediante una única arista saliente que regresa a sí misma. La función de etiquetado L define para cada estado s ∈ S el conjunto L ( s ) de todas las proposiciones atómicas que son válidas en s .

Un camino de la estructura M es una secuencia de estados ρ = s ₁ , s ₂ , s ₃ , ... tal que para cada i > 0 , se cumple R ( s _i , s _{i +1} ) . La palabra en el camino ρ es la secuencia de conjuntos de las proposiciones atómicas w = L ( s ₁ ), L ( s ₂ ), L ( s ₃ ), ... , que es una ω-palabra sobre el alfabeto 2 ^AP .

Con esta definición, una estructura de Kripke (por ejemplo, que tiene un solo estado inicial i ∈ I ) puede identificarse con una máquina de Moore con un alfabeto de entrada unitario, y con la función de salida siendo su función de etiquetado. ^{[ 4 ]}

Sea el conjunto de proposiciones atómicas AP = { p , q } . p y q pueden modelar propiedades booleanas arbitrarias del sistema que la estructura de Kripke está modelando.

La figura de la derecha ilustra una estructura de Kripke M = ( S , I , R , L ) , donde

• S = {s ₁ , s ₂ , s ₃ } .
• Yo = {s ₁ } .
• R = {(s ₁ , s ₂ ), (s ₂ , s ₁ ) (s ₂ , s ₃ ), (s ₃ , s ₃ )} .
• L = {(s ₁ , {p, q}), (s ₂ , {q}), (s ₃ , {p})} .

M puede producir una ruta ρ = s ₁ , s ₂ , s ₁ , s ₂ , s ₃ , s ₃ , s ₃ , ... y w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ... es la palabra de ejecución sobre la ruta ρ . M puede producir palabras de ejecución pertenecientes al lenguaje ({p, q}{q})*({p}) ^ω ∪ ({p, q}{q}) ^ω .

Aunque esta terminología está muy extendida en la comunidad de verificación de modelos, algunos libros de texto sobre verificación de modelos no definen la "estructura de Kripke" de esta manera tan amplia (o ni siquiera la definen), sino que simplemente utilizan el concepto de un sistema de transición (etiquetado) , que además tiene un conjunto de acciones Act , y la relación de transición se define como un subconjunto de S × Act × S , que además extienden para incluir un conjunto de proposiciones atómicas y una función de etiquetado para los estados ( L, como se definió anteriormente). En este enfoque, la relación binaria obtenida al abstraer las etiquetas de las acciones se denomina grafo de estados . ^{[ 5 ]}

Clarke et al. redefinen una estructura de Kripke como un conjunto de transiciones (en lugar de solo una), lo cual es equivalente a las transiciones etiquetadas anteriormente, cuando definen la semántica del μ-cálculo modal . ^{[ 6 ]}

• Lógica temporal
• Verificación de modelos
• Semántica de Kripke
• Lógica temporal lineal
• Lógica de árbol de computación