Tableaux for Policy Synthesis for MDPs with PCTL* Constraints

Baumgartner, P., Thiebaux, S., and Trevizan, F., Proc. of 26th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)

We are working on the camera-ready of this paper and it will be available in my website soon. Below is the abstract of this paper.

Markov decision processes (MDPs) are the standard formalism for modelling sequential decision making in stochastic environments. Policy synthesis addresses the problem of how to control or limit the decisions an agent makes so that a given specification is met. In this paper we consider PCTL*, the probabilistic counterpart of CTL*, as the specification language. Because in its full generality the policy synthesis problem for PCTL* is undecidable, we restrict to policies whose execution history memory is finitely bounded a priori. Surprisingly, no algorithm for policy synthesis for this natural and expressive framework has been developed so far. We close this gap and describe a corresponding algorithm. More precisely, we define a tableau calculus that, given an MDP and a PCTL* specification, derives in a non-deterministic way a system of (possibly nonlinear) equalities and inequalities. The solutions of this system, if any, describe the desired (stochastic, finite-memory) policies. Our main result in this paper is the correctness of our method, i.e., soundness, completeness and termination.

  • News and Highlights
    • h-pom, h-roc, and i2-dual won the best paper award at ICAPS'17!
    • New efficient approach to solve SSPs and C-SSPs with dead ends (UAI'17).
    • Solving SSPs and MDPs with PCTL* constraints to appear on TABLEAUX'17.
    • h-pom and h-roc: the first heuristics able to handle probabilities and costs for SSPs and C-SSPs (ICAPS'17).
    • i-dual won the best paper award at ICAPS'16!
    • QTM won the best paper award from the AI committee of TRB'16! (demo).
    • i-dual: combining AI and OR to efficiently solve constrained SSPs (ICAPS'16).
  • Word cloud of my papers:
  • wordcloud
    large wordcloud