Propozicná branching temporálna logika
CTL (Computational Tree Logic)
CTL? (Full Branching Time Logic) ? silnejšia ako CTL, historicky mladšia; najprv popíšeme CTL?
Syntax: (stavové a path („cestové“) formuly)
- kazdá atomická propozícia je stavová formula (S1)
- ak p, q sú stavové formuly, tak p ? q, ?p sú stavové formuly (S2)
- ak p je path formula, tak Ep, Ap sú stavové formuly(S3)
- kazdá stavová formula je aj path formula (P1)
- ak p, q sú path formuly, tak potom aj p ? q, ?p sú path formuly (P2)
- ak p, q sú path formuly, tak potom aj p ? q, Xp sú path formuly (P3)
CTL? tvoria stavové formuly
CTL tvoria pravidlá (S1), (S2), (S3) a pravidlo (P0):
- ak p, q sú stavové formuly, tak p ? q, Xp sú stavové formuly (P0)
A ? pre všetky budúcnosti
za A alebo E vzdy nasleduje jeden z operátorov G, F, X, ?
dá sa ukázat, ze CTL? má väcšiu vyjadrovaciu silu nez CTL