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 , kde je konečná množina stavov, je množina počiatočných stavov, je prechodová relácia, pre ktorú platí, že , 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 množinu L(s) atomických výrokov, ktoré v stave s platia.
Pozri aj
Temporálna logika Overovanie modelov Kripkeho sémantika
Iné projekty
Zdroj
Kategória:Matematická logika