Abstract:

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.

Short CV: Richard Mayr received a Msc in computer science from TU-Munich, Germany, (1994) and a PhD in computer science from TU-Munich (1998). He received scholarships from the DAAD and the DFG in support of his research at the University of Edinburgh, UK, (1999) and the University of Paris 7, France, (2000), and completed his Habilitation for Informatics at the University of Freiburg, Germany, in 2002. He was assistant professor at the University of Freiburg (2001-2004) and at North Carolina State University, USA, (2004-2007). In 2008 he was appointed to the post of Lecturer at the School of Informatics (LFCS) at the University of Edinburgh, UK. His research interests include automated verification, automata and temporal logic, model-checking and semantic equivalence checking, formal verification of real-time and probabilistic systems, infinite-state Markov chains and stochastic games.

--
Comunicaciones DCC