# Verification short course

From Murray Wiki

Jump to navigationJump to search### 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.

### 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:

- 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