Automatic Verification and Complexity of Systems under Probabilistic Uncertainty
My research is concerned with the computational complexity (and decidability) of probabilistic systems, in particular Markovian models such as Markov chains, Markov Decision Processes and stochastic games. The prototypical question addressed by the complexity theoretical framework is “How efficient can a given (mathematical) problem be solved by a computer?” Upper bounds on complexity are generally obtained by providing an algorithm for the problem at hand. In turn, lower bounds are proved via efficient reductions – algorithms transforming one problem into another – of previously studied problems. The study of computational complexity is thus intimately linked with the study of algorithms. As an important side product, one obtains ways to reformulate new problems into ones for which there already exist efficiently implemented well-tested algorithms. Hence complexity theory can also be viewed as a study of reusing existing algorithms in an efficient manner.
I am particularly interested in the following probabilistic models: Parametric Markov Decision Processes and Multi-Objective Stochastic Games.
In parametric Markov models such as Markov chains or MDPs, concrete probabilities may be replaced by real variables – the parameters. Parametric models are key to analyse situations were transition probabilities are unknown but not unrelated across the whole model; or to synthesise such probabilities in a way that a certain property holds. The main theoretical and practical difficulty of these models are the global dependencies between the parameters. One of my research goals is to establish the theoretical complexity of parametric MDPs and to identify expressive tractable subclasses.
I have also been working on stochastic two-person games with multiple objectives. In the context of probabilistic model checking, stochastic games are commonly used as a powerful abstraction mechanism to obtain sound bounds on quantitative properties of otherwise huge Markovian models. I have investigated complexity aspects of such games under lexicographic reachability objectives and conjunctions of thresholds on reachability properties.
The aim of this dissertation project is to pursue this line of work by studying various other probabilistic models or properties from a complexity point of view.