Algorithms for Analyzing and Verifying Infinite-State Recursive Probabilistic Systems

Abstract

Until recent years, research on automated verification and model checking of probabilistic systems was largely confined to using finite-state Markov chains (MCs) and finite-state Markov Decision processes (MDPs) as the core underlying models. In recent years, researchers have begun to develop new algorithms for, and study the computational complexity of, analysis and verification problems for classes of finitely-presented infinite-state probabilistic systems that arise as probabilistic extensions to classic infinite-state automata-theoretic models.