Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

12-2020

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

Keywords

Markov Chains, Cores, Complexity

Discipline

Software Engineering | Theory and Algorithms

Research Areas

Intelligent Systems and Optimization

Areas of Excellence

Digital transformation

Publication

Proceedings of the 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022), Chennai, India, December 18-20

Volume

250

First Page

1

Last Page

20

Identifier

10.4230/LIPICS.FSTTCS.2022.29

Publisher

Schloss Dagstuhl

City or Country

Germany

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29

Share

COinS