peter-2017.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -c 'year=2017 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2017.bib -oc peter-2017.cite peter.bib}}

@inproceedings{Baumgartner:etal:tableaux-policy-synthesis:TABLEAUX:2017,
  author = {Peter Baumgartner and Sylvie Thi{\'e}baux and Felipe Trevizan},
  title = {{Tableaux for Policy Synthesis for MDPs with PCTL* Constraints}},
  booktitle = {Tableaux 2017 -- Automated Reasoning with Analytic Tableaux and Related Methods},
  editor = {Renate A. Schmidt and Cl{\'a}udia Nalon},
  year = 2017,
  volume = 10501,
  series = {Lecture Notes in Artificial Intelligence},
  pages = {175--192},
  publisher = {Springer},
  url = {policy-synthesis-tableaux.pdf},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  abstract = {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 general 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 tableau-based algorithm 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) policies.
Our main result in this paper is the correctness of our method, i.e.,
soundness, completeness and termination.}
}

@article{Baumgartner:etal:tableaux-policy-synthesis-long:2017,
  author = {Peter Baumgartner and Sylvie Thi{\'e}baux and Felipe Trevizan},
  title = {Tableaux for Policy Synthesis for MDPs with PCTL* Constraints},
  journal = {CoRR},
  volume = {abs/1706.10102},
  year = {2017},
  url = {https://arxiv.org/abs/1706.10102},
  abstract = {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 general 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 tableau-based
                  algorithm 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)
                  policies.  Our main result in this paper is the correctness
                  of our method, i.e., soundness, completeness and
                  termination.}
}