67883 Formal verification of reactive systems (Fall 2009)
Lecture Notes
Temporal Logic
A proof
that AF(p /\ Xp) has no euivalent CTL formula