On Skolem-Hardness and Saturation Points in Markov Decision Processes

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragen

Abstract

The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic 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 non-classical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional value-at-risk for accumulated weights, and two problems addressing the long-run satisfaction of path properties, namely the optimization of long-run probabilities of regular co-safety properties and the model-checking problem of the logic frequency-LTL. To prove the Positivity- and hence Skolem-hardness for the latter two problems, a new auxiliary path measure, called weighted long-run frequency, is introduced and the Positivity-hardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with non-negative weights and for the optimization of long-run 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 value-at-risk for the classical SSPP and of weighted long-run frequencies on MDPs with non-negative weights can be solved in pseudo-polynomial time exploiting the existence of a saturation point. As a consequence, one obtains the decidability of the qualitative model-checking problem of a frequency-LTL formula that is not included in the fragments with known solutions.

Details

OriginalspracheEnglisch
Titel47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Redakteure/-innenArtur Czumaj, Anuj Dawar, Emanuela Merelli
Herausgeber (Verlag)Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Seiten138:1-138:17
ISBN (Print)978-3-95977-138-2
PublikationsstatusVeröffentlicht - 2020
Peer-Review-StatusNein

Publikationsreihe

Reihe47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) ; Bd. 168
ISSN1868-8969

Konferenz

Titel47th International Colloquium on Automata, Languages and Programming
KurztitelICALP 2020
Dauer8 - 11 Juli 2020
Webseite
Ortonline
StadtSaarbrücken
LandDeutschland

Externe IDs

Scopus 85089338467
ORCID /0000-0002-5321-9343/work/142236706
ORCID /0000-0003-4829-0476/work/165453934

Schlagworte

Schlagwörter

  • Markov decision process, Skolem problem, conditional value-at-risk, model checking, frequency-LTL, stochastic shortest path, conditional expectation, Markov decision process, Skolem problem, conditional value-at-risk, model checking, frequency-LTL