Affordable Access

Access to the full text

Algorithms and Hardness Results for Computing Cores of Markov Chains

Authors
  • Ahmadi, Ali
  • Chatterjee, Krishnendu
  • Goharshady, Amir Kafshdar
  • Meggendorfer, Tobias
  • Safavi, Roodabeh
  • Žikelić, Ðorđe
Publication Date
Jan 01, 2022
Identifiers
DOI: 10.4230/LIPIcs.FSTTCS.2022.29
OAI: oai:drops-oai.dagstuhl.de:17421
Source
Dagstuhl Research Online Publication Server
Keywords
Language
English
License
Green
External links

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.

Report this publication

Statistics

Seen <100 times