A really temporal logic

0. Introduction......Page 1 1. Reactive modules......Page 8 2. Invariant verification......Page 80 3. Symbolic graph search......Page 145 4. Graph minimization......Page 172 5. Real-time modules......Page 200 6. Safe temporal logic......Page 211 7. Safety automata......Page 243 8. Refinement verification......Page 265 9. Fair modules......Page 300 10. Response verification......Page 334 11. Live temporal logic......Page 356 12. Liveness automata......Page 383 13. Linear temporal logic......Page 405 99. Notation......Page 424