Estructura de Kripke

Este artícul descriu les estructures de Kripke com s'usen en Verificació de models. Per a una descripció més general, vore semàntiques de Kripke.

Una estructura de Kripke és una variació del sistema de transició, originalment proposta per Saul Kripke, usada en Verificació de models. per a representar el comportament d'un sistema. És bàsicament un grafo els nodos del qual representen estats alcanzables del sistema i les arestes del qual representen transicions d'estats. Una funció d'etiquetage mapea cada nodo a un conjunt de propietats que es complix en l'estat corresponent. Les llògiques temporals són interpretades tradicionalment en térmens d'estructures de Kripke.

Definició formal

Siga $A$ un conjunt de proposicions atòmiques , i.i. expressions booleanas sobre variables, constants i predicats. E. M. Clarke, O. Grumberg i D. A. Peled (1999) definixen una estructura de Kripke sobre $A$ com una 4-tupla $M=<S,I,R,L>$ a on:

• $S$ és un conjunt finito d'estats.
• $I\subseteq S$, un conjunt d'estats inicials .
• $R\subseteq S\times S$ és una relació de transició tal que, $\mathrm{\forall }s\in S,\mathrm{\exists }t\in S:(s,t)\in R$.
• una funció d'etiquetage (o interpretació) $L:S\to 𝒫(A)$.

Ya que $R$ és total, sempre és possible construir una sendera infinita a través de l'estructura de Kripke. La funció d'etiquetage $L$ definix per a cada estat $s\in S$ el conjunt $L(s)$ de totes les proposicions atòmiques que són vàlides en $s$.

Una sendera de l'estructura $M$ és una seqüència d'estats $p=s_1,s_2,s_3\mathrm{...}$, tal que per a cada $i>0$, es complix $R(s_i,s_{i+1})$. La traça sobre la sendera ρ és la seqüència de conjunts de proposicions atòmiques $w=L(s_1),L(s_2),L(s_3)$..., que és una ω-traça sobre l'alfabet $𝒫(A)$.

En esta definició, una estructura de Kripke pot identificar-se en una Màquina de Moore en un alfabet d'entrada unitari, i en la funció d'eixida sent la seua funció d'etiquetage.

Eixemple

Archiu:Estructura de Kripke.jpg

Eixemple senzill d'una estructura de Kripke.

Siga $AP=\{p,q,r\}$ el conjunt de proposicions atòmiques.

La figura de la dreta ilustra una estructura de Kripke $M=(S,I,R,L)$, a on

• $S=\{s_1,s_2,s_3\}$.
• $I=\{s_1\}$.
• $R=\{(s_1,s_2),(s_2,s_3)(s_3,s_2),(s_3,s_1)\}$.
• $L=\{(s_1,\{p\}),(s_2,\{p,q\}),(s_3,\{r\})\}$.

$M$ pot produir la sendera $p=s_1,s_2,s_3,s_2,s_3,s_1$. $w=\{p\},\{p,q\},\{r\},\{p,q\},\{r\},\{p\}$ és la traça d'eixecució sobre dit sendera. $M$ pot produir paraules pertanyents al llenguage $(\{p\},(\{p,q\},\{r\}{)}^{*})$^ω.

Vore també

• Llògica temporal
• Verificació de models