Verification short course

Lecture 1: Automata Theory (2 hours)

Topics:

• Finite transition systems
• Paths, traces and composition of finite transition systems
• Linear time properties; safety and liveness
• Examples

Reading:

• Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. Chapters 2 and 3.

Lecture 2: Temporal Logic (2 hours)

Topics:

• Linear temporal logic
• Omega regular properties (liveness, fairness)
• Buchi automata, representation of LTL using NBA
• Examples

Reading:

• Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. Chapters 4 and 5.

Lecture 3: Model Checking (2 hours)

Topics:

• Basic concepts in model checking
• Explicit model checking (SPIN)
• Symbolic model checking (nuSMV)
• Probabilistic modeling checking (PRISM)
• Examples

Reading:

• Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. Chapter 5.

Lecture 4: Logic Synthesis (2 hours)

Topics:

• Use of model checking for logic synthesis
• Examples

Lecture 5: Algorithmic Verification of Hybrid Systems

Topics:

• Abstraction hierarchies for control systems
• Finite state abstractions (discretization) and model checking
• Discretization of continuous state systems
• Approximate bi-simulation (if time)
• Examples

Reading:

• TBD

Lecture 6: Synthesis of Reactive Control Protocols

Topics:

• Open system and reactive system synthesis
• Satisfiability, realizability
• Game structures, reachability/safety games
• Mu-calculus (if time) and GR(1) games
• Examples

Reading:

• On the development of reactive systems, D. Harel and A. Pnueli, Logics and models of concurrent systems, Springer-Verlag New York, Inc., 1985, pp. 477–498. For discussion about closed and open systems

Computer Session 2: TuLiP

• Introduction to TuLiP
• Synthesis of protocols for discrete systems
• Discretization of continuous systems (and protocol synthesis)
• Examples