---
res:
bibo_abstract:
- 'Given a Markov chain M = (V, v_0, δ), with state space V and a starting state
v_0, 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 ℙ[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 [Jan Kretínský
and Tobias Meggendorfer, 2020]. 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.@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Ali
foaf_name: Ahmadi, Ali
foaf_surname: Ahmadi
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Amir Kafshdar
foaf_name: Goharshady, Amir Kafshdar
foaf_surname: Goharshady
foaf_workInfoHomepage: http://www.librecat.org/personId=391365CE-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0003-1702-6584
- foaf_Person:
foaf_givenName: Tobias
foaf_name: Meggendorfer, Tobias
foaf_surname: Meggendorfer
foaf_workInfoHomepage: http://www.librecat.org/personId=b21b0c15-30a2-11eb-80dc-f13ca25802e1
orcid: 0000-0002-1712-2165
- foaf_Person:
foaf_givenName: Roodabeh
foaf_name: Safavi Hemami, Roodabeh
foaf_surname: Safavi Hemami
foaf_workInfoHomepage: http://www.librecat.org/personId=72ed2640-8972-11ed-ae7b-f9c81ec75154
- foaf_Person:
foaf_givenName: Dorde
foaf_name: Zikelic, Dorde
foaf_surname: Zikelic
foaf_workInfoHomepage: http://www.librecat.org/personId=294AA7A6-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4681-1699
bibo_doi: 10.4230/LIPIcs.FSTTCS.2022.29
bibo_volume: 250
dct_date: 2022^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/1868-8969
- http://id.crossref.org/issn/9783959772617
dct_language: eng
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Algorithms and hardness results for computing cores of Markov chains@
...