Kripke struktuur
Dünaamiline loogika
Dünaamiline loogika on modaalloogika erijuht, mis arutleb programmide käitumise üle. Dünaamiline loogika on mitmemodaalne, modaalsused indekseeritud toimingutega. Dünaamilise loogika signatuur (signature) koonseb kahest tähestikust PC = {p, q, ...} ja AC = {a, b, ...}, mille sümboleid nimetatakse vastavalt lausesümboliteks ja toimingusümboliteks.
Las AP = {p,q} olla lausesümbolite hulk (atomic propositions), kus p ja q modeleerivad suvalisi Kripke struktuuri kirjeldatud süsteemi Boole'i omadusi, näiteks Boole'i tehtele omistatud väärtusi.
Kripke struktuur
Kripke struktuur on mitte-deterministlik automaat (non-deterministic automata). Temporaalloogikat rakendatakse traditsiooniliselt Kripke struktuuril. Kripke struktuuri nimetatakse ka sildistatud olekumasinaks. Kripke struktuuris on kaks tähtsat nõuet:
- ülemineku seos peab olema terviklik (transition-relation must be complete) ning
- kasutusel on sildistamisfunktsioon (labelling function) mis tagastab igas oleku puhul kehtivad lausesümbolid omadused.
Ajaline loogika on tüüpiliselt kirjeldatud Kripke struktuuri ehk sildistatud üleminekute süsteemi (labeled transition system) abil Kripke struktuur on kirja pandud kui:
Milles S on lõplik olekute hulk:
T on ülemineku seos:
Sₒ on algsete olekute hulk:
L on sildistamise funktsioon. Sildistamise funktsioon tagastab omadused mis on tõesed selles olekus. (L(s) set of atomic propositions that are true in s). Võib eeldada et omadused mida sildistamise funktsioon ei tagasta on täitmata.
Kripke struktuuris peab igal olekul olema väljaminev ülemineku seos, öeldakse ka et ülemineku seos peab olema terviklik. Selle tingimuse täitmiseks piisab väljaminevast seosest tagasi iseendale:
Kripke struktuuris aeg on reaalarv (?).