Propozicná branching temporálna logika
(S1) M, s0 ? p iff p ? L(s0)
(S2) M, s0 ? p ? q iff platí M, s0 ? p and M, s0 ? q
M, s0 ? ?p iff neplatí M, s0 ? p
(S3) M, s0 ? Ep iff ?x v M tak, ze M, x ? p
M, s0 ? Ap iff pre ?x v M platí M, x ? p
(P1) M, x ? p iff M, s0 ? p
(P2) M, x ? p ? q iff platí M, x ? p and M, x ? q
M, x ? ?p iff neplatí M, x ? p
?j (M, xj ? q a ?k (k < j implikuje M, xk ? p)