Kripke model

Kripkes model ( eng. Kripke structure ) er en af varianterne af en ikke-deterministisk finit automat, som blev foreslået af Saul Kripke . Denne form for NFA bruges til at teste modeller for at repræsentere et systems adfærd.

Kripke-modellen er en simpel abstrakt maskine, der gør det muligt at beskrive en computermaskines ideer uden at tilføje megen kompleksitet. Modellen er repræsenteret ved en rettet graf , hvis toppunkter beskriver de nåbare tilstande af systemet, og kanterne beskriver overgangene fra tilstand til tilstand.

Etiketfunktionen tildeler hvert toppunkt et sæt egenskaber, der udføres i den tilsvarende tilstand.

Formel definition

Lad være et sæt atomudsagn (booleske udtryk over et sæt variabler, konstanter og prædikatsymboler). Kripke-modellen [1] er en firedobbelt bestående af: $AP$ $M = (S,\;I,\;R,\;L)$

et begrænset sæt af tilstande ; $S\;$
sæt af begyndelsestilstande ; $I \subseteq S$
overgangsforhold , hvor sådan ; $R\subseteq S\! \ gange\! S\;$ $\; \forall s \! \i\! S, \; \eksisterer s^' \!\! \i\! S$ $(s,s^') \i R$
markup funktioner . $L: S \rightarrow 2^{AP}$

Betingelsen pålagt relationen R siger, at hver stat har følgende. Hvis du vil efterligne en dødvande , skal du i Kripke-modellen blot tilføje en kant fra blokeringstilstanden til sig selv.

Markeringsfunktionen L for hver tilstand s ∈ S bestemmer mængden L ( s ) af alle atomare udsagn sande i s .

Se også

Noter

↑ Clark E. M., Gramberg O., Peled D. Verifikation af programmodeller. Modelkontrol. Moskva: MTsNMO. 2002.