On Skolem-Hardness and Saturation Points in Markov Decision Processes

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributed

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

Original languageEnglish
Title of host publication47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
EditorsArtur Czumaj, Anuj Dawar, Emanuela Merelli
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages138:1-138:17
ISBN (print)978-3-95977-138-2
Publication statusPublished - 2020
Peer-reviewedNo

Publication series

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

Conference

Title47th International Colloquium on Automata, Languages and Programming
Abbreviated titleICALP 2020
Duration8 - 11 July 2020
Website
Locationonline
CitySaarbrücken
CountryGermany

External IDs

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

Keywords

Keywords

  • 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