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