Probabilistic model checking for discrete-Time Markovian models

Christel Baier

The tutorial presents the basic principles of discrete-time Markov chains and Markov decision processes. It will explain the syntax and semantics of probabilistic computation tree logic (PCTL and PCTL*), the automata-based quantitative analysis and the main steps of the PCTL/PCTL* model checking procedure.