Semantics and Verification

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:
  • 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
  • Linear-Time properties (part. 1)
    • Deadlocks
    • Invariants
    • Checking for invariant with Reachability algorithm


• Course 2 (February 7th)
  
  • Linear-Time 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 model-checking transition systems
    • ω-regular expressions
    • Nondeterministic Büchi automata: equivalence with ω-regular languages
    • Deterministic Büchi automata: non-equivalence with ω-regular languages
    • Generalized nondeterministic Büchi automata,
      • Equivalence with NBA
      • closure under intersection


• Course 4 (February 28th)
  
  • Model-checking ω-regular properties
    • Emptiness of NBA, complexity
    • Product of Transition System with NBA
    • Model-checking 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, Release-PNF
    • Fairness in LTL
    • From LTL to GNBA
    • General construction
    • Applying it to ○a and aUb
    • Optimality: exponential lower bound for LTL->NBA
    • PSPACE-completeness of LTL model-checking, satisfiability, validity
    • A regular language that is not LTL-definable
  • A regular language L such that L^ω is not DBA-recognizable


• 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
  • Model-Checking algorithm for CTL: description and complexity


• Course 7 (March 28th)
  
  • Fairness in CTL
    • Fairness formulas
    • Complexity
  • CTL*
  • Syntax and semantics: state formulas and path formulas
  • Expressivity (versus CTL and LTL)
  • Model-Checking algorithm for CTL*: description and complexity
  • Bisimulation
  • Bisimulation relation for transition systems
  • Bisimulation quotient
  • Action-based bisimulation
  • Relationship with CTL*/CTL equivalence


• 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


• Course 9 (April 11th)
  
  • Probabilistic Computation Tree Logic (PCTL)
    • Syntax and Semantics
    • Model-checking

Back home.