Kripkeho štruktúra

Kripkeho štruktúra, pomenovaná po Saulovi Kripkem, je druh nedeterministického konečného automatu, používaného najmä v overovaní modelov na reprezentáciu správania systému. V podstate ide o graf, ktorého vrcholy (alebo uzly) reprezentujú dosiahnuteľné stavy systému, a ktorého hrany predstavujú prechody. Ohodnocovacia funkcia priraďuje každému uzlu množinu vlastností, ktoré v zodpovedajúcom stave platia. Temporálne logiky sa zvyčajne interpretujú v zmysle Kripkeho štruktúr.

Formálna definícia

Nech AP je množina tzv. atomických výrokov, teda boolovských výrazov nad danými premennými, konštantami a predikátovými symbolmi.

Kripkeho štruktúra je usporiadaná štvorica $M=(S,I,R,L)$, kde

• $S$ je konečná množina stavov,
• $I\subseteq S$ je množina počiatočných stavov,
• $R\subseteq S\times S$ je prechodová relácia, pre ktorú platí, že $\mathrm{\forall }s\mathrm{\exists }{s}^{\prime }:(s,s^{\prime })\in R$,
• $L:S\to 2^{AP}$ je ohodnocovacia funkcia.

Keďže je relácia R zľava úplná, je vždy možné nájsť v danej Kripkeho štruktúre nekonečnú cestu. To znamená, že zo stavu uviaznutia vychádza práve jedna hrana smerujúca späť do daného stavu.

Ohodnocovacia funkcia L definuje pre každý stav $s\in S$ množinu L(s) atomických výrokov, ktoré v stave s platia.

Pozri aj

• Temporálna logika
• Overovanie modelov
• Kripkeho sémantika