CMPE 278: Topics for final exam
Fall 2004

The final exam will be open books and open notes, and they will cover the following topics:
  1. Reactive modules. How to model a system via reactive modules.
  2. Safety and reachability verification; enumerative algorithms.
  3. BDDs, and algorithms for BDDs.
  4. Symbolic algorithms for reachability and safety analysis. Computation of the Pre, Post operators.
  5. mu-calculus notation for symbolic algorithms.
  6. Simulation and bisimulation. Definitions, and game-theoretic characterization.
  7. Enumerative and symbolic algorithms for simulation and bisimulation.
  8. Construction of abstractions by variable hiding.
  9. CTL and system specification.
  10. Symbolic model-checking of CTL specifications via the mu-calculus.
  11. Relation between ACTL and simulation, and between CTL and bisimulation.
  12. LTL.
  13. Omega automata, in particular, Streett and Buchi automata.
  14. Translation from LTL to automata, and automata-theoretic verification.