Long-run Satisfaction of Path Properties
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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
Original language | English |
---|---|
Title of host publication | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Publisher | IEEE, New York [u. a.] |
Number of pages | 14 |
ISBN (print) | 978-1-7281-3608-0 |
Publication status | Published - 2019 |
Peer-reviewed | Yes |
Conference
Title | 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 |
---|---|
Duration | 24 - 27 June 2019 |
City | Vancouver |
Country | Canada |
External IDs
ORCID | /0000-0002-5321-9343/work/142236713 |
---|---|
Scopus | 85070745741 |
ORCID | /0000-0003-4829-0476/work/165453935 |
Keywords
Keywords
- Long-run satisfaction, path properties