Cours de Spécialisation M2

Références bibliographiques:

• "Model Checking for probability and time: from theory to practice", Marta Kwiatkowska, 18th Annnual IEEE Symposium on Logic in Computer Science (LICS'03), page 351
• "Probabilistic model checking: formalisms and algorithms for discrete and real-time systems", C. Courcoubetis and S. Tripakis. In M. K. Inan and R. P. Kurshan, editors, Verification of Digital and Hybrid Systems, pages 183--219. Springer, 2000.
• "Logiques temporelles et Automates", cours M2 de Hubert Common.
• "An automata-theoretic approach to linear time temporal logic", M. Vardi. VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata
• An automata-theoretic approach to branching time model-checking", O. Kupferman, M. Vardi, P. Wolper, Computer Aided Verification (CAV'94)

1ière partie: Olivier Bournez

• Séance 1: (3h).
  • Logiques et Automates.
• Séance 2: (3h).
  • Vérification Algorithmique de Systèmes Probabilistes.

2ième partie: Stephan Merz

Clicker ici

Bonus

• Raisonnements Compositionnels
• Réductions d'ordre partiel
• Systèmes Hybrides (ces slides sont dans un état très provisoire)