Verification of Infinite-State Probabilistic Systems

Richard Mayr

Sala P303 Philippe Flajolet (3er. piso edificio poniente) DCC, UChile.

14:30 22/08/2017

Probabilistic program models can be used to describe systems that exhibit uncertainty, such as communication protocols over unreliable channels, randomized algorithms in distributed systems, or fault-tolerant systems. Their semantics can be defined in terms of Markov chains, Markov decision processes or stochastic games. The usage of resources (time, power, memory, bandwidth, etc.) can be modeled by assigning a reward (or cost) to individual transitions, or, more generally, to whole computation paths. The resulting Markov reward model can be analyzed to verify safety, liveness and performance properties.  For example: "What is the distribution/expectation/variance  of the time/cost needed to reach a given target state?  More generally, such properties can be expressed in stochastic logics for probabilistic systems (e.g., PCTL, and PRCTL) and verified by model checking techniques. We give an overview over new techniques for verifying quantitative properties of general infinite-state probabilistic systems (with unbounded counters, buffers, process creation, or recursion). These techniques use special structural properties of the underlying system models, such as sequential decomposition, finite attractors, or partial orders and monotonicity properties.