Lecturer: 王凡 Farn Wang

• LTL
• CTL, CTL*
• Expressivenss
• LTL satisfiability: tableau-based techniques
• CTL model-checking
• Simulation-checking
• ATL and game graphs
• ATL model-checking

• Temporal Logics & Model Checking [slides]

• Exercise 1
• Exercise 2
• Exercise 3