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.
LDAP: couldn't connect to LDAP server