Abstract

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 specifications with the structure of branching-time temporal logics. We provide a systematic presentation of results on decidability and complexity of the model-checking problem for these logics together with a detailed presentation of some verification techniques. Possibly the most important original results of this work concerning temporal logics are decidability of the model-checking problem for the qualitative fragment of PECTL* and undecidability of the same problem for PCTL. The class of long-run average properties is very useful in performance and reliability analysis of systems. These properties are tightly connected with service cycles and can be used to answer questions like: Is the average time of servicing a request lower than a given bound? In this work we define a whole class of such properties, and study decidability and complexity of the problem whether a given system satisfies these properties. We also study a notion of predictability of long-run average properties based on observing a finite part of a computation of the system. We show that all properties from our class are effectively predictable up to a given error tolerance. …víceméně