Office of Academic Affairs
Indian Institute of Science Education and Research Bhopal

ECS 615: Probabilistic Model Checking (4)

Learning Objectives:

Formal verification is the process of checking whether a design satisfies some requirements (properties). Model checking is the most popular method for automatic formal verification of safety critical software and hardware systems. It can be used to assess both qualitative and quantitative properties of complex systems. This course focuses on the fundamentals of model checking for probabilistic/stochastic models. These models are typically used to capture the behavior of systems that are subject to uncertainties, e.g., randomized distributed algorithms, queuing systems, economics, dynamic power management in embedded systems and systems biology. 

We will discuss model checking algorithms for several probabilistic models and present equivalence relations for comparing the behavior of these probabilistic models.

Course Contents:

• Discrete-time Markov chains (DTMCs) and reachability probabilities
• Applications of DTMCs 
• Model checking algorithms for probabilistic linear temporal logic (PLTL)
• Model checking algorithms for probabilistic computation tree logic (PCTL)
• Probabilistic bisimulation
• Discrete-time Markov decision processes (DMDPs) and reachability probabilities
• Applications of DMDPs
• PCTL model checking on DMDPs
• Continuous-time Markov chains (CTMCs), rewards, transient analysis and timed-reachability probabilities
• Applications of CTMCs
• Continuous stochastic logic (CSL) model checking on CTMCs
• Probabilistic automata (PAs) and Interactive Markov chains (IMCs)

Selected Readings:

• C. Baier and J.-P. Katoen. Principles of Model Checking, MIT Press, 2008.
• H. Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. LNCS 2428, Springer 2002.

Papers:

• M. Kwiatkowska et al. Stochastic model checking. Proceedings of the 7th international conference on Formal methods for performance evaluation, Pages 220-270, 2007.
• M. Stoelinga: Introduction to Probabilistic Automata. Bulletin of the EATCS 78. 2002.
• PRISM Model Checker - http://www.prismmodelchecker.org/manual/Main/AllOnOnePage
• J P Katoen et al. Comparative branching-time semantics for Markov chains. Inf. Comput., 2005.
• J P Katoen et al. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng., 2003.

---

Previous

Back to Course List

Next