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.}
}