Verification of Probabilistic Recursive Sequential Programs

This work studies algorithmic verification of infinite-state probabilistic systems generated by probabilistic pushdown automata (pPDA). Probabilistic pushdown automata are obtained as a probabilistic variant of pushdown automata that proved to be a successful abstract model of recursive sequential programs. The main aim of this work is to study decidability and complexity of the problem whether a given probabilistic system generated by a pPDA satisfies a given property expressed in a suitable formalism. There are plenty of formalisms available for specifying properties of probabilistic systems. In this work we consider various temporal properties expressed by finite-state automata on infinite words and formulae of temporal logics, long-run average properties, and properties connected with expected behavior. Concerning temporal logics, we consider both linear and branching time ones. Among others we consider linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), which is a probabilistic variant of the well-known logic CTL. We also consider a general logic PECTL ∗ , which combines automata based