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.
cs-486/topics-and-objectives.txt · Last modified: 2017/09/05 15:50 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0