Algorithms and hardness results for computing cores of Markov chains

• Main Authors: AHMADI, Ali, CHATTERJEE, Krishnendu, KAFSHDAR GOHARSHADY, Amir, MEGGENDORFER, Tobias, SAFAVI, Roodabeh, ZIKELIC, Dorde
• 格式: text
• 語言: English
• 出版: Institutional Knowledge at Singapore Management University 2020
• 主題: Markov Chains; Cores; Complexity; Software Engineering; Theory and Algorithms
• 在線閱讀: https://ink.library.smu.edu.sg/sis_research/9059; https://ink.library.smu.edu.sg/context/sis_research/article/10062/viewcontent/Algorithms_and_Hardness_Results.pdf
• 機構: Singapore Management University

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 f ind a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset.