## 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: |