Modelo kripke

El modelo de Kripke ( eng. Estructura de Kripke ) es una de las variantes de un autómata finito no determinista, que fue propuesto por Saul Kripke . Este tipo de NFA se utiliza para probar modelos para representar el comportamiento de un sistema.

El modelo de Kripke es una máquina abstracta simple que permite describir las ideas de una máquina de cómputo sin agregar mucha complejidad. El modelo está representado por un gráfico dirigido , cuyos vértices describen los estados alcanzables del sistema y los bordes describen las transiciones de un estado a otro.

La función de etiqueta asigna a cada vértice un conjunto de propiedades que se ejecutan en el estado correspondiente.

Formal definición

Sea un conjunto de sentencias atómicas (expresiones booleanas sobre un conjunto de variables, constantes y símbolos de predicados). El modelo de Kripke [1] es un cuádruple que consta de: $punto de acceso$ $M = (S,\;I,\;R,\;L)$

un conjunto finito de estados ; $S\;$
conjuntos de estados iniciales ; $I \subseteq S$
relaciones de transición , cuando tales que ; $R\subconjunto S\! \veces\! S\;$ $\; \para todos \! \en\! S, \; \existen s^' \!\! \en\! S$ $(s,s^') \en R$
funciones de marcado $L: S \rightarrow 2^{AP}$

La condición impuesta a la relación R establece que cada estado tiene lo siguiente. Si desea emular un interbloqueo , en el modelo de Kripke solo necesita agregar un borde desde el estado de bloqueo a sí mismo.

La función de marca L para cada estado s ∈ S determina el conjunto L ( s ) de todas las declaraciones atómicas verdaderas en s .

Véase también

Notas

↑ Clark E. M., Gramberg O., Peled D. Verificación de modelos de programas. Comprobación de modelos. Moscú: MTsNMO. 2002.