Carrying Probabilistic Reasoning to the Infinite World: On the Verification of Infinite-State Markov Chains

Abstract: This seminar is an overview of the research we have done during the last five years on model checking of probabilistic systems.
In recent years, several approaches have been proposed for automatic verification of infinite-state systems. In a parallel development, there has been an extensive research effort for the design and analysis of models with stochastic behaviors. We consider verification of Markov chains with infinite state spaces. We describe a general framework that can handle probabilistic versions of several classical models such as Petri nets, communicating processes, push-down automata, and noisy Turing machines. We consider both safety, liveness, and limiting behavior problems for these classes of systems. Furthermore, we describe algorithms to solve general versions of the problems in the context of stochastic games.