Final published version
Licence: CC BY: Creative Commons Attribution 4.0 International License
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Publication date | 14/12/2022 |
---|---|
Host publication | 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022 |
Editors | Anuj Dawar, Venkatesan Guruswami |
Pages | 29:1-29:20 |
Number of pages | 20 |
ISBN (electronic) | 9783959772617 |
<mark>Original language</mark> | English |
Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 250 |
ISSN (Print) | 1868-8969 |
Given a Markov chain M = (V, v0, δ), with state space V and a starting state v0, and a probability threshold ϵ, an ϵ-core is a subset C of states that is left with probability at most ϵ. More formally, C ⊆ V is an ϵ-core, iff P [reach (V \C)] ≤ ϵ. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ϵ-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ϵ-core of a given size is NP-complete. This solves an open problem posed in [26]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ϵ-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset.