Estructura de Kripke

Una estructura de Kripke es una variación del sistema de transición, originalmente propuesta por Saul Kripke,[1]​ usada en Verificación de modelos.

[2]​ para representar el comportamiento de un sistema.

Es básicamente un grafo cuyos nodos representan estados alcanzables del sistema y cuyas aristas representan transiciones de estados.

Una función de etiquetado mapea cada nodo a un conjunto de propiedades que se cumple en el estado correspondiente.

Las lógicas temporales son interpretadas tradicionalmente en términos de estructuras de Kripke.

un conjunto de proposiciones atómicas , i.e.

expresiones booleanas sobre variables, constantes y predicados.

E. M. Clarke, O. Grumberg y D. A. Peled (1999)[3]​ definen una estructura de Kripke sobre

{\displaystyle M=}

es total, siempre es posible construir un sendero infinito a través de la estructura de Kripke.

La función de etiquetado

{\displaystyle L(s)}

de todas las proposiciones atómicas que son válidas en

Un sendero de la estructura

es una secuencia de estados

{\displaystyle R(s_{i},s_{i+1})}

La traza sobre el sendero ρ es la secuencia de conjuntos de proposiciones atómicas

..., que es una ω-traza sobre el alfabeto

Con esta definición, una estructura de Kripke 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.

= { p , q , r }

el conjunto de proposiciones atómicas.

La figura de la derecha ilustra una estructura de Kripke

{\displaystyle M=(S,I,R,L)}

es la traza de ejecución sobre dicho sendero.

puede producir palabras pertenecientes al lenguaje