 Courses by Denis Kuperberg
 Tutorials by Laureline Pinault

The course is based on the book:
 Baier, C. and Katoen, J.P., Principles of Model Checking, MIT Press, 2008.
Courses

Course 1 (January 29th)
 General overview of the course.

Modelling Concurrent Systems
 Labelled Transition Systems
 Modelling Logical Circuits
 Interleaving, Handshaking, Parallel Composition, Synchronous Product

LinearTime properties (part. 1)
 Deadlocks
 Invariants
 Checking for invariant with Reachability algorithm

Course 2 (February 7th)

LinearTime properties (part.2)
 Trace Inclusion/equivalence
 Safety properties
 Liveness properties
 Link with topology

LinearTime properties (part.2)

Course 3 (February 14th)
 Fairness Assumptions

Regular Properties

Safety regular properties,
 Representation via NFA for bad prefixes
 Algorithm for modelchecking transition systems
 ωregular expressions
 Nondeterministic Büchi automata: equivalence with ωregular languages
 Deterministic Büchi automata: nonequivalence with ωregular languages

Generalized nondeterministic Büchi automata,
 Equivalence with NBA
 closure under intersection

Safety regular properties,

Course 4 (February 28th)

Modelchecking ωregular properties
 Emptiness of NBA, complexity
 Product of Transition System with NBA
 Modelchecking Persistence properties

Linear Temporal Logic (part 1)
 Syntax and Semantic
 Equivalence laws
 Fixpoint characterizations
 Weak Until, Positive Normal Form

Modelchecking ωregular properties

Course 5 (March 7th)

Linear Temporal Logic (part 2)
 Release operator, ReleasePNF
 Fairness in LTL
 From LTL to GNBA
 General construction
 Applying it to ○a and aUb
 Optimality: exponential lower bound for LTL>NBA
 PSPACEcompleteness of LTL modelchecking, satisfiability, validity
 A regular language that is not LTLdefinable
 A regular language L such that L^{ω} is not DBArecognizable

Linear Temporal Logic (part 2)

Course 6 (March 21st)

Deterministic Parity Automata (DPA)
 Definition
 Equivalence with NBA (DPA>NBA proved, NBA>DPA admitted)
 Hierarchy of parity conditions
 Computation Tree Logic (CTL)
 Syntax and semantics: state formulas and path formulas
 Theorem for translating CTL to LTL when possible
 Incomparability of CTL with LTL
 Equivalence laws, Existential Normal Form
 ModelChecking algorithm for CTL: description and complexity

Deterministic Parity Automata (DPA)
 Course 7 (March 28th)

Fairness in CTL
 Fairness formulas
 Complexity
 CTL*
 Syntax and semantics: state formulas and path formulas
 Expressivity (versus CTL and LTL)
 ModelChecking algorithm for CTL*: description and complexity
 Bisimulation
 Bisimulation relation for transition systems
 Bisimulation quotient
 Actionbased bisimulation
 Relationship with CTL*/CTL equivalence

Fairness in CTL
 Course 8 (April 4th)

Probabilistic Systems
 Markov Chains
 LTL events and their probability measure
 Constrained reachability (C Until B) probability computation
 Qualitative Properties: almost sure (repeated) reachability

Probabilistic Systems
 Course 9 (April 11th)

Probabilistic Computation Tree Logic (PCTL)
 Syntax and Semantics
 Modelchecking

Probabilistic Computation Tree Logic (PCTL)
Back home.