Model checking
- daná štruktúra M a formula p
Úloha: zistit, ci M je modelom pre p
Branching?Time?Logic?Model?Checking
- daná konecná štruktúra M = (S, R, L) a BTL formula p
Úloha: pre kazdý stav s ? S urcit, ci platí M, s? p a ak áno, s sa oznací znackou “p”
Linear?Time?Logic?Model?Checking
- daná konecná štruktúra M = (S, R, L) a LTL formula p
Úloha: pre kazdý stav s ? S urcit, ci existuje plná cesta, splnajúca p, zacínajúca sa v s, a ak áno, s sa oznací “Ep”
Príklad: CTL model checking
- predpokladajme, ze uz máme vrcholy, pre ktoré platí “p oznacené”
- ideme oznacovat tie, pre ktoré platí AFp:
1. ak je vrchol oznacený p, tak ho oznacíme aj AFp
2. (opakuje sa, kým sa dá)
oznac vrchol s AFp, ak všetci jeho následníci sú oznacení AFp
3. oznac ?AFp tie, ktoré nie sú oznacené AFp