Lectures

• Lecture 1: Modelling systems slides1 and slides2
• Lecture 2: Linear-time Properties slides
• Lecture 3: Regular Safety Properties slides
• Reading Liveness and Fairness from slide 52, and read also Chapter 3 Sections 3.4 and 3.5 of PoM
• Lecture 4: Büchi Automata slides
• Lecture 5: Linear-time temporal Logic slides + Linear-time properties: notion of fairness slides
• Lecture 6: Verifying regular safety properties slides, extended version, see also Section 4.4 of PoM.
• Reading End of lecture 6 on DFS nested algorithm, with associated Section 4.4.2 page 203 of PoM.
• Lecture 7: Linear-time temporal Logic model checking slides and Decision problems on LTL slides
• Lecture 8: Branching-time Logics slides1 and slides2
• Lecture 9: CTL model checking slides and an short intro to CTL*
• Lecture 10: Bisimulation slides
• Lecture 11 Flipped classroom Hour 1:
  • LTL vs CTL
  • Clarke, E. M., and Draghicescu, I. A. (1988, May). Expressibility results for linear-time and branching-time logics. In Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems) (pp. 428-437). Springer, Berlin, Heidelberg.
• Lecture 11 Flipped classroom Hour 2:
  • Fairness in LTL
  • Fairness in CTL
  • + other slides
• Lecture 12 Flipped classroom Hour 1:
  • CTL* and CTL+
  • CTL* model-checking
• Lecture 12 Flipped classroom Hour 2:
  • Complexity bounds of all decision problems (MC, SAT, VALID), see the book PoM

TD/TP

• TD1 Introduction to Concurrency and Channel systems
• TP1 You will need the files process.smv, semaphore.smv, and TP1.smv.
• TD2
• TP2 You will need the file TP2.smv
• TD3
• TP3 You will need the file filo.smv
• TD4
• TP4 Evaluation 1
• TD5
• TP5
• TD6
• TP6 Evaluation 2