Long-run Satisfaction of Path Properties

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-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 languageEnglish
Title of host publication2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherIEEE, New York [u. a.]
Number of pages14
ISBN (print)978-1-7281-3608-0
Publication statusPublished - 2019
Peer-reviewedYes

Conference

Title34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Duration24 - 27 June 2019
CityVancouver
CountryCanada

External IDs

ORCID /0000-0002-5321-9343/work/142236713

Keywords

Keywords

  • Long-run satisfaction, path properties