TY - GEN

T1 - Algorithms and Hardness Results for Computing Cores of Markov Chains.

AU - Ahmadi, Ali

AU - Chatterjee, Krishnendu

AU - Goharshady, Amir Kafshdar

AU - Meggendorfer, Tobias

AU - Safavi, Roodabeh

AU - Zikelic, Ðorde

PY - 2022/12/14

Y1 - 2022/12/14

N2 - 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.

AB - 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.

KW - Complexity

KW - Cores

KW - Markov Chains

U2 - 10.4230/LIPIcs.FSTTCS.2022.29

DO - 10.4230/LIPIcs.FSTTCS.2022.29

M3 - Conference contribution/Paper

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 29:1-29:20

BT - 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022

A2 - Dawar, Anuj

A2 - Guruswami, Venkatesan

ER -