Estructura de Kripke

Este artículo describe las estructuras de Kripke como se usan en Verificación de modelos. Para una descripción más general, ver semánticas 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.

Definición formal

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]​

Ejemplo

 

Ejemplo sencillo de una estructura de Kripke.

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\})^{*})}$ ^ω.

Véase también

• Lógica temporal
• Verificación de modelos

Referencias

1. Kripke, Saul (1963). «Semantical Considerations on Modal Logic». Acta Philosophica Fennica (16): 83-94. ISSN 0355-1792. 
2. Clarke, Edmund (2008). «The Birth of Model Checking». En O. Grumberg y H. Veith (Eds.), ed. The Birth of Model Checking. Vol. 5000: Lecture Notes in Computer Science. Berlín - Heidelberg: Springer. pp. 1-26. ISBN 978-3-540-69850-0. 
3. Clarke, E. M.; Grumberg, O.; Peled, D. A. (1999). Model Checking. MA: The MIT Press. p. 14. ISBN 9780262032704. 
4. Schneider, Klaus (2004). Verification of reactive systems: formal methods and algorithms. Springer. p. 45. ISBN 978-3-540-00296-3. 

•   Datos: Q1077740
•   Multimedia: Kripke models