Murray: Created page with "=== Lecture 1: Automata Theory (2 hours) === Topics: * Finite transition systems * Paths, traces and composition of finite transition systems * Linear time properties; safety ..."

2012-11-03T16:51:46Z

Created page with "=== Lecture 1: Automata Theory (2 hours) === Topics: * Finite transition systems * Paths, traces and composition of finite transition systems * Linear time properties; safety ..."

New page

=== 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:
* <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 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:
* [http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 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:
* [http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. Chapter 5.

=== Computer Session: nuSMV (2 hours) ===

=== 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:
* [http://portal.acm.org/citation.cfm?id=101990 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</p>

=== Computer Session 2: TuLiP ===
* Introduction to TuLiP
* Synthesis of protocols for discrete systems
* Discretization of continuous systems (and protocol synthesis)
* Examples

Verification short course - Revision history

Murray: Created page with "=== Lecture 1: Automata Theory (2 hours) === Topics: * Finite transition systems * Paths, traces and composition of finite transition systems * Linear time properties; safety ..."