Symbolic Time and Space Tradeoffs for Probabilistic Verification

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(2)) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(n root m) symbolic operations and O(root m) symbolic space. The main open question has been whether the worst-case O(n(2)) bound for symbolic operations can be beaten for MEC decomposition computation. In this work, we answer the open question in the affirmative. We present a symbolic algorithm that requires (O) over tilde (n(1.5)) symbolic operations and (O) over tilde (root n) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0 < is an element of <= 1/2 the symbolic algorithm requires <(O)over tilde> (n(2-is an element of)) symbolic operations and (O) over tilde (n(is an element of)) symbolic space ((O) over tilde (center dot) hides polylogarithmic factors). Using our techniques we also present faster algorithms for computing the almost-sure winning regions of w -regular objectives for MDPs. We consider the canonical parity objectives for !-regular objectives, and for parity objectives with d-priorities we present an algorithm that computes the almost-sure winning region with (O) over tilde (n(2-is an element of)) symbolic operations and (O) over tilde (n(is an element of)) symbolic space, for all 0 < is an element of <= 1/2. In contrast, previous approaches require either (a) O(n(2) center dot d) symbolic operations and O(log n) symbolic space; or (b) O(n root m center dot d) symbolic operations and O(root m) symbolic space. Thus we improve the time-space product from <(O)over tilde>(n(2) center dot d) to (O) over tilde (n(2)).