Introduction to Probabilistic Model Checking

Prof. Christel Baier, Technische Universität Dresden, Alemania

Markov chains (MC) and Markov decision processes (MDP) are widely used as operational models for the quantitative system analysis. They can be understood as transition systems augmented with distributions for the states (in MC) or state-action pairs (in MDPs) to specify the probabilities for the successor states. Additionally one might add weight functions for modeling accumulated costs or rewards earned along path fragments to represent e.g. the energy consumption, the penality to be paid for missed deadlines, the gain for completing tasks successfully or the degree of the achieved utility.

The tutorial will introduce the main features of discrete-time, finite-state Markovian models (MC and MDP) and their quantitative analysis against temporal logic specifications. The first part will present the basic princi- ples of the automata-based approach for linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), including a summary of tech- niques that have been proposed to tackle the state-explosion problem. The second part of the tutorial will present algorithms for dealing with fairness assumptions and computing conditional probabilities and quantiles.

Material Bibliográfico: