A student should be able to do the following at the completion of CS 486

- Modeling systems:
- Develop concurrent models in the PROMELA language
- Describe how a Kripke structure can be used to model a transition system.
- Demonstrate how a single Kripke structure can model a concurrent system with several different components.
- Describe the difference between synchronous and interleaving semantics and their impact on parallel composition.
- Identify systems that would use synchronous over interleaving semantics.
- Describe how a system in a high-level language can be transformed into a Kripke structure.

- Temporal logic
- Describe the differences between CTL*, CTL, and LTL temporal logic.
- Write temporal logic to define basic properties.
- Describe what path quantifiers are used for.
- Describe what temporal operators are used for.
- Demonstrate the expressive limitations of CTL and LTL logics as compared to CTL*.
- Describe fairness and why it is needed in model checking.

- Model Checking CTL
- Demonstrate how to convert arbitrary CTL formulas to only use NOT, OR, EX, EU, and EG.
- Describe the algorithm to label states in a Kripke structure for EU formulas.
- Describe the algorithm to label states in a Kripke structure for EG forumlas.
- Explain the complexity bound for CTL model checking and where it comes from.
- Describe the changes to the basic CTL labeling algorithms to verify systems with fairness constraints.

- Ordinary binary decision diagrams (OBDDs)
- Explain the use of OBDDs.
- Draw the basic structure of an OBDD.
- List the properties of an OBDD in its canonical form.
- Show how to combine OBDDs using Boolean connectives.
- Represent a Kripke structure using an OBDD.
- Describe the relative strengths and weaknesses of OBDDs and properties that affect their time and space complexity.

- Symbolic Model Checking
- Characterize CTL operators as least or greatest fixed points of an appropriate predicate transformer.
- Show how OBDDs can be used for model checking.
- Describe how to implement fairness constraints in symbolic model checking.
- Show how to obtain a witness or counterexample to a property in symbolic model checking.

- Model checking and automata theory.
- Verify properties of PROMELA models using the SPIN model checker
- Describe the difference between finite automata and Buchi automata.
- Explain the need for Buchi automata in LTL model checking.
- Describe the role of nondeterminism in model checking.
- Explain the double depth-first search algorithm and how it used to in model checking.
- Define the term on-the-fly model checking and describe what it does.
- Explain how fairness constraints can be added to LTL model checking.