Branching temporálna logika
temporálna štruktúra: trojica M = (S, R, L), kde
R ? S ? S taká, ze ?s ? S ?t ? S (s, t) ? R
L: S ? ?(AP) ? urcuje pre daný stav, ktoré atomické propozície v tomto stave platia (teda ktoré AP sú true)
M mozno chápat ako znackovaný orientovaný graf s vrcholmi S, hranami danými R a vrcholy majú znacky dané L
Hovoríme, ze M je
- acyklický, ak nemá orientované cykly
- stromová štruktúra, ak kazdý vrchol má nanajvýš jedného predchodcu
- strom, ak je stromová štruktúra a má koren
oznacenie:
- plná cesta x = (s0, s1, s2, s3, …): pre ?i: (si, si+1) ? R
- definujeme xi = (si, si+1, si+2, si+3, … )