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

editar

Sea   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   como una 4-tupla   donde:

  •   es un conjunto finito de estados.
  •  , un conjunto de estados iniciales .
  •   es una relación de transición tal que,  .
  • una función de etiquetado (o interpretación)  .

Dado que   es total, siempre es posible construir un sendero infinito a través de la estructura de Kripke. La función de etiquetado   define para cada estado   el conjunto   de todas las proposiciones atómicas que son válidas en  .

Un sendero de la estructura   es una secuencia de estados  , tal que para cada  , se cumple  . 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.[4]

Ejemplo

editar
 
Ejemplo sencillo de una estructura de Kripke.

Sea   el conjunto de proposiciones atómicas.

La figura de la derecha ilustra una estructura de Kripke  , donde

  •  .
  •  .
  •  .
  •  .

  puede producir el sendero  .   es la traza de ejecución sobre dicho sendero.   puede producir palabras pertenecientes al lenguaje  ω.

Véase también

editar

Referencias

editar
  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.