Piribauer, Jakob ;
Baier, Christel
On SkolemHardness and Saturation Points in Markov Decision Processes
Abstract
The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding numbertheoretic problems whose decidability has been open for many decades. In this paper, the inherent mathematical difficulty of a series of optimization problems on Markov decision processes (MDPs) is shown by a reduction from the Positivity problem to the associated decision problems which establishes that the problems are also at least as hard as the Skolem problem as an immediate consequence. The optimization problems under consideration are two nonclassical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional valueatrisk for accumulated weights, and two problems addressing the longrun satisfaction of path properties, namely the optimization of longrun probabilities of regular cosafety properties and the modelchecking problem of the logic frequencyLTL. To prove the Positivity and hence Skolemhardness for the latter two problems, a new auxiliary path measure, called weighted longrun frequency, is introduced and the Positivityhardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with nonnegative weights and for the optimization of longrun probabilities of constrained reachability properties (aU b), solutions are known that rely on the identification of a bound on the accumulated weight or the number of consecutive visits to certain sates, called a saturation point, from which on optimal schedulers behave memorylessly. In this paper, it is shown that also the optimization of the conditional valueatrisk for the classical SSPP and of weighted longrun frequencies on MDPs with nonnegative weights can be solved in pseudopolynomial time exploiting the existence of a saturation point. As a consequence, one obtains the decidability of the qualitative modelchecking problem of a frequencyLTL formula that is not included in the fragments with known solutions.
BibTeX  Entry
@InProceedings{piribauer_et_al:LIPIcs:2020:12545,
author = {Jakob Piribauer and Christel Baier},
title = {{On SkolemHardness and Saturation Points in Markov Decision Processes}},
booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
pages = {138:1138:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771382},
ISSN = {18688969},
year = {2020},
volume = {168},
editor = {Artur Czumaj and Anuj Dawar and Emanuela Merelli},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12545},
URN = {urn:nbn:de:0030drops125455},
doi = {10.4230/LIPIcs.ICALP.2020.138},
annote = {Keywords: Markov decision process, Skolem problem, stochastic shortest path, conditional expectation, conditional valueatrisk, model checking, frequencyLTL}
}
29.06.2020
Keywords: 

Markov decision process, Skolem problem, stochastic shortest path, conditional expectation, conditional valueatrisk, model checking, frequencyLTL 
Seminar: 

47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Issue date: 

2020 
Date of publication: 

29.06.2020 