Kripkeho štruktúra

z Wikipédie, slobodnej encyklopédie
Prejsť na: navigácia, hľadanie

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[upraviť | upraviť zdroj]

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 \forall s\  \exists s': (s,s') \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[upraviť | upraviť zdroj]

Zdroj[upraviť | upraviť zdroj]

Tento článok je čiastočný alebo úplný preklad článku Kripke structure na anglickej Wikipédii.