Home > Research > Publications & Outputs > Algorithms and Hardness Results for Computing C...

Links

Text available via DOI:

View graph of relations

Algorithms and Hardness Results for Computing Cores of Markov Chains.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
  • Ali Ahmadi
  • Krishnendu Chatterjee
  • Amir Kafshdar Goharshady
  • Tobias Meggendorfer
  • Roodabeh Safavi
  • Ðorde Zikelic
Close
Publication date14/12/2022
Host publication42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022
EditorsAnuj Dawar, Venkatesan Guruswami
Pages29:1-29:20
Number of pages20
ISBN (electronic)9783959772617
<mark>Original language</mark>English

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume250
ISSN (Print)1868-8969

Abstract

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.