Long-run Satisfaction of Path Properties

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

Beitragende

Abstract

The paper introduces the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We then study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold. The main results are as follows. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the threshold problem.

Details

OriginalspracheEnglisch
Titel2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Herausgeber (Verlag)IEEE, New York [u. a.]
Seitenumfang14
ISBN (Print)978-1-7281-3608-0
PublikationsstatusVeröffentlicht - 2019
Peer-Review-StatusJa

Konferenz

Titel34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Dauer24 - 27 Juni 2019
StadtVancouver
LandKanada

Externe IDs

ORCID /0000-0002-5321-9343/work/142236713
Scopus 85070745741
ORCID /0000-0003-4829-0476/work/165453935

Schlagworte

Schlagwörter

  • Long-run satisfaction, path properties