Algorithms and hardness results for computing cores of Markov chains

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 p...

Full description

Saved in:
Bibliographic Details
Main Authors: AHMADI, Ali, CHATTERJEE, Krishnendu, KAFSHDAR GOHARSHADY, Amir, MEGGENDORFER, Tobias, SAFAVI, Roodabeh, ZIKELIC, Dorde
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2020
Subjects:
Online Access: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
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-10062
record_format dspace
spelling sg-smu-ink.sis_research-100622024-08-01T15:34:19Z Algorithms and hardness results for computing cores of Markov chains AHMADI, Ali CHATTERJEE, Krishnendu KAFSHDAR GOHARSHADY, Amir MEGGENDORFER, Tobias SAFAVI, Roodabeh ZIKELIC, Dorde 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. 2020-12-01T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9059 info:doi/10.4230/LIPICS.FSTTCS.2022.29 https://ink.library.smu.edu.sg/context/sis_research/article/10062/viewcontent/Algorithms_and_Hardness_Results.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Markov Chains Cores Complexity Software Engineering Theory and Algorithms
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Markov Chains
Cores
Complexity
Software Engineering
Theory and Algorithms
spellingShingle Markov Chains
Cores
Complexity
Software Engineering
Theory and Algorithms
AHMADI, Ali
CHATTERJEE, Krishnendu
KAFSHDAR GOHARSHADY, Amir
MEGGENDORFER, Tobias
SAFAVI, Roodabeh
ZIKELIC, Dorde
Algorithms and hardness results for computing cores of Markov chains
description 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.
format text
author AHMADI, Ali
CHATTERJEE, Krishnendu
KAFSHDAR GOHARSHADY, Amir
MEGGENDORFER, Tobias
SAFAVI, Roodabeh
ZIKELIC, Dorde
author_facet AHMADI, Ali
CHATTERJEE, Krishnendu
KAFSHDAR GOHARSHADY, Amir
MEGGENDORFER, Tobias
SAFAVI, Roodabeh
ZIKELIC, Dorde
author_sort AHMADI, Ali
title Algorithms and hardness results for computing cores of Markov chains
title_short Algorithms and hardness results for computing cores of Markov chains
title_full Algorithms and hardness results for computing cores of Markov chains
title_fullStr Algorithms and hardness results for computing cores of Markov chains
title_full_unstemmed Algorithms and hardness results for computing cores of Markov chains
title_sort algorithms and hardness results for computing cores of markov chains
publisher Institutional Knowledge at Singapore Management University
publishDate 2020
url 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
_version_ 1814047720046854144