Sea ${\displaystyle A}$  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 A}$  como una 4-tupla ${\displaystyle M=<S,I,R,L>}$  donde:

• ${\displaystyle S}$  es un conjunto finito de estados.
• ${\displaystyle I\subseteq S}$ , un conjunto de estados iniciales .
• ${\displaystyle R\subseteq S\times S}$  es una relación de transición tal que, ${\displaystyle \forall s\in S,\exists t\in S:(s,t)\in R}$ .
• una función de etiquetado (o interpretación) ${\displaystyle L:S\to {\mathcal {P}}(A)}$ .

Dado que ${\displaystyle R}$  es total, siempre es posible construir un sendero infinito a través de la estructura de Kripke. La función de etiquetado ${\displaystyle L}$  define para cada estado ${\displaystyle s\in S}$  el conjunto ${\displaystyle L(s)}$  de todas las proposiciones atómicas que son válidas en ${\displaystyle s}$ .

Un sendero de la estructura ${\displaystyle M}$  es una secuencia de estados ${\displaystyle p=s_{1},s_{2},s_{3}...}$ , tal que para cada ${\displaystyle i>0}$ , se cumple ${\displaystyle R(s_{i},s_{i+1})}$ . La traza sobre el sendero ρ es la secuencia de conjuntos de proposiciones atómicas ${\displaystyle w=L(s_{1}),L(s_{2}),L(s_{3})}$ ..., que es una ω-traza sobre el alfabeto ${\displaystyle {\mathcal {P}}(A)}$ .

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.^[4]​

Sea ${\displaystyle AP=\{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)}$ , donde

• ${\displaystyle S=\{s_{1},s_{2},s_{3}\}}$ .
• ${\displaystyle I=\{s_{1}\}}$ .
• ${\displaystyle R=\{(s_{1},s_{2}),(s_{2},s_{3})(s_{3},s_{2}),(s_{3},s_{1})\}}$ .
• ${\displaystyle L=\{(s_{1},\{p\}),(s_{2},\{p,q\}),(s_{3},\{r\})\}}$ .

${\displaystyle M}$  puede producir el sendero ${\displaystyle p=s_{1},s_{2},s_{3},s_{2},s_{3},s_{1}}$ . ${\displaystyle w=\{p\},\{p,q\},\{r\},\{p,q\},\{r\},\{p\}}$  es la traza de ejecución sobre dicho sendero. ${\displaystyle M}$  puede producir palabras pertenecientes al lenguaje ${\displaystyle (\{p\},(\{p,q\},\{r\})^{*})}$ ^ω.

• Lógica temporal
• Verificación de modelos