FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Distribution-based objectives for Markov Decision Processes

Authors: S. Akshay, Blaise Genest and Nikhil Vyas

Paper Information

Title:Distribution-based objectives for Markov Decision Processes
Authors:S. Akshay, Blaise Genest and Nikhil Vyas
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:games and logic, model checking, probabilistic systems, Markov decision processes, probabilistic finite automata, Distribution based objectives, Kakutani's fixed point theorem
Abstract:

ABSTRACT. We consider distribution-based objectives for Markov Decision Processes (MDP). This class of objectives gives rise to an interesting trade-off between full and partial information. As in full observation, the strategy in the MDP can depend on the state of the system, but similar to partial information, the strategy needs to account for all the states at the same time.

In this paper, we focus on two safety problems that arise naturally in this context, namely, existential and universal safety. Given an MDP A and a closed and convex polytope H of probability distributions over the states of A, the existential safety problem asks whether there exists some distribution ∆ in H and a strategy of A, such that starting from ∆ and repeatedly applying this strategy keeps the distribution forever in H. The universal safety problem asks whether for all distributions in H, there exists such a strategy of A which keeps the distribution forever in H. We prove that both problems are decidable, with tight complexity bounds: we show that existential safety is PTIME-complete, while universal safety is co-NP-complete.

Further, we compare these results with existential and universal safety problems for Rabin’s probabilistic finite-state automata (PFA), the subclass of Partially Observable MDPs which have zero observation. Compared to MDPs, strategies of PFAs are not state dependent. In sharp contrast to the PTIME result, we show that existential safety for PFAs is undecidable. On the other hand, it turns out that the universal safety for PFAs is decidable in EXPTIME, with a co-NP lower bound. Finally, we show that an alternate representation of the input polytope allows us to improve the complexity of universal safety for MDPs and PFAs.

Pages:10
Talk:Jul 10 15:40 (Session 57B)
Paper: