- Este artículo describe las estructuras de Kripke que se utilizan en la verificación de modelos. Para obtener una descripción más general, consulte Semántica de Kripke .
Una estructura de Kripke es una variación del sistema de transición , propuesto originalmente por Saul Kripke , [1] utilizado en la verificación de modelos [2] para representar el comportamiento de un sistema. Consiste en un gráfico cuyos nodos representan los estados alcanzables del sistema y cuyos bordes representan transiciones de estado, junto con una función de etiquetado que asigna cada nodo a un conjunto de propiedades que se mantienen en el estado correspondiente. Las lógicas temporales se interpretan tradicionalmente en términos de estructuras de Kripke. [ cita requerida ]
Definicion formal
Sea AP un conjunto de proposiciones atómicas , es decir, expresiones booleanas sobre variables, constantes y símbolos de predicado. Clarke y col. [3] define una estructura de Kripke sobre AP como una tupla de 4 M = ( S , I , R , L ) que consta de
- un conjunto finito de estados S .
- un conjunto de estados iniciales I ⊆ S .
- una relación de transición R ⊆ S × S tal que R es -total que queda , es decir, ∀s ∈ S ∃s' ∈ S tal que (s, s') ∈ R .
- una función de etiquetado (o interpretación ) L : S → 2 AP .
Dado que R es total a la izquierda , siempre es posible construir un camino infinito a través de la estructura de Kripke. Un estado de interbloqueo se puede modelar mediante un solo borde saliente de regreso a sí mismo. La función de etiquetado L define para cada estado s ∈ S el conjunto L ( s ) de todas las proposiciones atómicas que son válidas en s .
Un camino de la estructura M es una secuencia de estados ρ = s 1 , s 2 , s 3 , ... tal que para cada i> 0 , se cumple R (s i , s i + 1 ) . La palabra en el camino ρ es una secuencia de conjuntos de proposiciones atómicas w = L (s 1 ), L (s 2 ), L (s 3 ), ... , que es una palabra ω sobre el alfabeto 2 AP .
Con esta definición, una estructura de Kripke (digamos, que tiene solo un estado inicial i ∈ I ) puede identificarse con una máquina de Moore con un alfabeto de entrada singleton, y con la función de salida siendo su función de etiquetado. [4]
Ejemplo
Sea el conjunto de proposiciones atómicas AP = {p, q} . p y q pueden modelar propiedades booleanas arbitrarias del sistema de que la estructura de Kripke está modelando.
La figura de la derecha ilustra una estructura de Kripke M = ( S , I , R , L ) , donde
- S = {s 1 , s 2 , s 3 } .
- I = {s 1 } .
- R = {(s 1 , s 2 ), (s 2 , s 1 ) (s 2 , s 3 ), (s 3 , s 3 )} .
- L = {(s 1 , {p, q}), (s 2 , {q}), (s 3 , {p})} .
M puede producir una ruta ρ = s 1 , s 2 , s 1 , s 2 , s 3 , s 3 , s 3 , ... y w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ... es la palabra de ejecución sobre la ruta ρ . M puede producir palabras de ejecución que pertenecen al lenguaje ({p, q} {q}) * ({p}) ω ∪ ({p, q} {q}) ω .
Relación con otras nociones
Aunque esta terminología está muy extendida en la comunidad de verificación de modelos, algunos libros de texto sobre verificación de modelos no definen la "estructura de Kripke" de esta manera extendida (o en absoluto de hecho), sino que simplemente utilizan el concepto de un sistema de transición (etiquetado) , que además tiene un Acto de acciones establecido, y la relación de transición se define como un subconjunto de S × Act × S , que además se extienden para incluir un conjunto de proposiciones atómicas y una función de etiquetado para los estados también ( L como se define arriba). En este enfoque, la relación binaria obtenida al abstraer las etiquetas de acción se denomina gráfico de estado . [5]
Clarke y col. redefinir una estructura de Kripke como un conjunto de transiciones (en lugar de solo una), que es equivalente a las transiciones etiquetadas arriba, cuando definen la semántica del cálculo μ modal . [6]
Ver también
Referencias
- ^ Kripke, Saul, 1963, "Consideraciones semánticas sobre la lógica modal", Acta Philosophica Fennica, 16: 83-94
- ^ Clarke, Edmund M. (2008): El nacimiento del control de modelos. en: Grumberg, Orna y Veith, Helmut eds .: 25 Years of Model Checking, vol. 5000: Notas de la conferencia en Ciencias de la Computación. Springer Berlín Heidelberg, pág. 1-26.
- ^ Clarke, Edmund M., Jr; Grumberg, Orna; Peled, Doron (diciembre de 1999). Comprobación del modelo . Serie de sistemas ciberfísicos. Prensa del MIT. pag. 14. ISBN 9780262032704.
- ^ Klaus Schneider (2004). Verificación de sistemas reactivos: métodos formales y algoritmos . Saltador. pag. 45. ISBN 978-3-540-00296-3.
- ^ Christel Baier ; Joost-Pieter Katoen (2008). Principios de verificación de modelos . La prensa del MIT. pp. 20 -21 y 94-95. ISBN 978-0-262-02649-9.
- ^ Clarke y col. pag. 98