Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives

DOI10.1007/S10703-012-0180-2MaRDI QIDQ2248060zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Manas Joglekar, Nisarg Shah, Monika R. Henzinger

Publication date 30 June 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1104.3348

zbMATH Keywords

Büchi objectivesMarkov decision processesprobabilistic verificationsymbolic algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Symbolic computation and algebraic computation (68W30) Markov and semi-Markov decision processes (90C40)

Abstract: We consider Markov decision processes (MDPs) with omega-regular specifications given as parity objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. The algorithms for the computation of the almost-sure winning set for parity objectives iteratively use the solutions for the almost-sure winning set for B"uchi objectives (a special case of parity objectives). Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with B"uchi objectives; our algorithm takes O(n sqrt{m}) symbolic steps as compared to the previous known algorithm that takes O(n^2) symbolic steps, where $n$ is the number of states and $m$ is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n sqrt{n}) symbolic steps, as compared to the previous known $O(n^2)$ symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n sqrt{K}) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5n symbolic steps, whereas our new algorithm takes 4n symbolic steps.

Recommendations

• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• Computer Science Logic
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• scientific article; zbMATH DE number 1786649

Cites work

• A data structure for dynamic trees
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Code aware resource management
• Computer Science Logic
• Distributed algorithms for SCC decomposition
• Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification
• scientific article; zbMATH DE number 3148886 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 1134975 (Why is no real title available?)
• scientific article; zbMATH DE number 2079387 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Magnifying-Lens Abstraction for Markov Decision Processes
• Model checking of probabilistic and nondeterministic systems
• Number of quantifiers is better than number of tape cells
• Quantitative stochastic parity games
• The complexity of probabilistic verification
• Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study

Cited in

(11)

• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• Optimal cost almost-sure reachability in POMDPs
• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• Trading performance for stability in Markov decision processes
• Büchi objectives in countable MDPs
• Measuring and synthesizing systems in probabilistic environments
• An \(O(n^2)\) time algorithm for alternating Büchi games
• Symbolic algorithms for graphs and Markov decision processes with fairness objectives
• Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth
• CEGAR for compositional analysis of qualitative properties in Markov decision processes

Describes a project that uses

Uses Software

• CUDD

This page was built for publication: Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2248060)