Kripke modell

A Kripke-modell ( angol. Kripke-struktúra ) egy nem-determinisztikus véges automata egyik változata, amelyet Saul Kripke javasolt . Ezt a fajta NFA-t a rendszer viselkedését reprezentáló modellek tesztelésére használják.

A Kripke-modell egy egyszerű absztrakt gép, amely lehetővé teszi egy számítástechnikai gép gondolatainak leírását anélkül, hogy bonyolultabbá tenné. A modellt egy irányított gráf reprezentálja , melynek csúcsai a rendszer elérhető állapotait, élei pedig az állapotból állapotba való átmeneteket írják le.

A címke függvény minden csúcshoz hozzárendel egy tulajdonságkészletet, amely a megfelelő állapotban kerül végrehajtásra.

Formális definíció

Legyen atomi utasítások halmaza (logikai kifejezések változók, konstansok és predikátumszimbólumok halmazán). A Kripke modell [1] egy négyes , amely a következőkből áll: $AP$ $M = (S,\;I,\;R,\;L)$

állapotok véges halmaza ; $S\;$
kezdeti állapotok halmazai ; $I \subseteq S$
átmeneti relációk , ahol ilyen ; $R\subseteq S\! \times\! S\;$ $\; \forall s \! \ban ben\! S, \; \exist s^' \!\! \ban ben\! S$ $(s,s^') \in R$
jelölő funkciók . $L: S \jobbra 2^{AP}$

Az R relációra támasztott feltétel kimondja, hogy minden állapot rendelkezik a következőkkel. Ha patthelyzetet szeretne emulálni , a Kripke modellben csak hozzá kell adnia egy élt a blokkoló állapotból önmagához.

Az L jelölőfüggvény minden s ∈ S állapothoz meghatározza az összes igaz atomi állítás L ( s ) halmazát s -ben .

Lásd még

Jegyzetek

↑ Clark E. M., Gramberg O., Peled D. Programmodellek ellenőrzése. Modellellenőrzés. Moszkva: MTsNMO. 2002.