Model Checking and Decision Procedures for Probabilistic Automata and Markov Chains

Finite-state probabilistic automata were introduced by Michael Rabin in the 1960s and have recently been the subject of renewed interest. In the first half of this tutorial we review classical results and open problems on the complexity of decision problems for probabilistic automata, including the analogs of language inclusion, language equivalence and language emptiness.