Symbolic Time and Space Tradeoffs for Probabilistic Verification

2021/04/15 by Chatterjee, Krishnendu, Dvořák, Wolfgang, Henzinger, Monika +1 · 1 citation
#Computer Science and Game Theory (cs.GT) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2104.07466

Abstract

We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n²) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(n √(m)) symbolic operations and O(√(m)) symbolic space. A main open question is whether the worst-case O(n²) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires \widetildeO(n^1.5) symbolic operations and \widetildeO(√(n)) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0

Cited by

• INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition

Related

• Faster Algorithms for Markov Decision Processes with Low Treewidth
• INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
• Symbolic Algorithms for Graphs and Markov Decision Processes with\n Fairness Objectives
• Verifying Reachability Properties in Markov Chains via Incremental Induction
• Leveraging the Power of Graph Algorithms: Efficient Algorithms for Computer-Aided Verification