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.