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 enUn sendero de la estructuraes 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 alfabetoCon 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
