References

 
  • Model checking real-time systems: Timed Automata.
  • The model checker Spin: Spin online references.
  • Safety and liveness: Defining livenesss by Alpern and Schneider.
  • The model checker Spin: Spin online references.
  • Temporal Logic (LTL and CTL): Handbook of theoretical computer science, Vol.2, Chapter 16: Temporal and Modal Logic by E. A. Emesron
  • Buchi automata: Handbook of theoretical computer science, Vol.2, Chapter 4: Automata on Infinite Words by W. Thomas.
  • Propositional and predicate logic: Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. Second Edition (available at Google Books).
  • PVS: The PVS documentation at SRI website.