M1 IF course, second semester, 2018,
ENS de Lyon.
Wednesday 13:30  15:30.
 Courses by Denis Kuperberg

Tutorials by Laureline Pinault

The course is based on the book:
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

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

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

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

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
Back home.