Abstract

Probabilistic methods are widely used in the design, analysis, and verification of computer systems that exhibit some kind of uncertainty such as coin-tossing in randomized algorithms, subsystem failures (caused, e.g., by communication errors or bit flips with an empirically evaluated probability), or underspecification in some components of the system. Verification methods have been developed mainly for finite-state probabilistic systems, that cannot always faithfully model real situations. Hence, the thesis focuses on verification problems for a wider class of probabilistic systems, namely probabilistic recursive sequential programs represented by probabilistic pushdown automata. Some decidability and complexity questions concerning model-checking problems for probabilistic temporal logics and probabilistic pushdown automata are studied. The thesis also introduces several limit properties of runs of probabilistic systems, and studies decidability and complexity of verification of these properties for the probabilistic pushdown automata. The aim of the thesis is to develop theoretical tools for specification and verification of the probabilistic recursive sequential programs. …víceméně