## 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 (a U 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.

Original language | English |
---|---|

Title of host publication | 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020 |

Editors | Artur Czumaj, Anuj Dawar, Emanuela Merelli |

Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |

ISBN (Electronic) | 9783959771382 |

DOIs | |

State | Published - 1 Jun 2020 |

Externally published | Yes |

Event | 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020 - Virtual, Online, Germany Duration: 8 Jul 2020 → 11 Jul 2020 |

### Publication series

Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|

Volume | 168 |

ISSN (Print) | 1868-8969 |

### Conference

Conference | 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020 |
---|---|

Country/Territory | Germany |

City | Virtual, Online |

Period | 8/07/20 → 11/07/20 |

## Keywords

- Conditional expectation
- Conditional value-at-risk
- Frequency-LTL
- Markov decision process
- Model checking
- Skolem problem
- Stochastic shortest path