Controller Synthesis for Markov Decision Processes with Branching-Time Objectives
| Authors | |
|---|---|
| Year of publication | 2009 |
| MU Faculty or unit | |
| Citation | |
| Description | This thesis studies controller synthesis and verification problems for finite state Markov decision processes and branching-time logics. Markov decision processes are probabilistic systems that arise naturally in modelling of real-life systems with both nondeterministic and stochastic behaviour, while branching-time logics are formalisms allowing one to reason about properties of systems. The controller synthesis problem asks, given a Markov decision process and a formula of branching-time logic, whether there is a controller that ensures satisfying the formula. The verification problem is defined dually, i.e. asks whether the formula is satisfied under all controllers. Various fragments of controller synthesis and verification problems may be obtained by restricting the use of memory and/or randomization in the controller, or by considering different logics and their fragments. Main goal of this thesis is to present current knowledge about these problems and to provide their classification. We consider logics PCTL, PCTL* and PECTL*, where the first two logics are probabilistic counterparts of the well-known logics CTL and CTL*, and PECTL* is a branching-time logic that uses Büchi automata instead of conventional temporal operators. We show that the controller synthesis problem is undecidable even when the formulae to be satisfied are PCTL formulae and we ask for a deterministic finite-memory controller only. On the other hand, we identify several subproblems that are decidable and of practical interest. The decidability results are twofold. We study memoryless controllers, where we extend known results from PCTL to the stronger logics. We also study qualitative fragments of logics, where we show that controllers may need to use possibly unbounded counter in order to be winning, and the set of probabilities they assign to a transition during a play may be infinite. This is possibly the most demanding part of this thesis, where we show that the memory provided by one-counter automaton is sufficient and give the decidability result for the problem. For many of the studied subproblems, we also provide matching lower complexity bounds. |
| Related projects: |