TY - CONF AB - A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution. AU - Kretinsky, Jan AU - Meggendorfer, Tobias AU - Weininger, Maximilian ID - 13967 SN - 1043-6871 T2 - 38th Annual ACM/IEEE Symposium on Logic in Computer Science TI - Stopping criteria for value iteration on stochastic games with quantitative objectives VL - 2023 ER - TY - CONF AB - 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(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of ω -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˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 . AU - Chatterjee, Krishnendu AU - Dvorak, Wolfgang AU - Henzinger, Monika H AU - Svozil, Alexander ID - 10002 KW - Computer science KW - Computational modeling KW - Markov processes KW - Probabilistic logic KW - Formal verification KW - Game Theory SN - 1043-6871 T2 - Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science TI - Symbolic time and space tradeoffs for probabilistic verification ER - TY - CONF AB - Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs. AU - Chatterjee, Krishnendu AU - Doyen, Laurent ID - 10004 KW - Computer science KW - Heuristic algorithms KW - Memory management KW - Automata KW - Markov processes KW - Probability distribution KW - Complexity theory SN - 1043-6871 T2 - Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science TI - Stochastic processes with expected stopping time ER - TY - CONF AB - We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces AU - Henzinger, Thomas A ID - 4519 SN - 1043-6871 T2 - Proceedings 11th Annual IEEE Symposium on Logic in Computer Science TI - The theory of hybrid automata ER -