Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
From MaRDI portal
Publication:3189650
DOI10.1145/2597631zbMath1295.91019OpenAlexW2005353519MaRDI QIDQ3189650
Krishnendu Chatterjee, Monika R. Henzinger
Publication date: 12 September 2014
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2597631
Noncooperative games (91A10) Games involving graphs (91A43) Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Graph algorithms (graph-theoretic aspects) (05C85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
Finding 2-Edge and 2-Vertex Strongly Connected Components in Quadratic Time ⋮ Graph Games and Reactive Synthesis ⋮ Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes ⋮ Trading performance for stability in Markov decision processes ⋮ Fine-grained complexity lower bounds for problems in computer aided verification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications ⋮ Unnamed Item ⋮ Generic Emptiness Check for Fun and Profit ⋮ Combinations of Qualitative Winning for Stochastic Parity Games ⋮ Algorithms and conditional lower bounds for planning problems ⋮ Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components ⋮ Quantitative fair simulation games ⋮ Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games ⋮ Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Measuring and Synthesizing Systems in Probabilistic Environments ⋮ Looking at mean-payoff and total-payoff through windows ⋮ Optimal cost almost-sure reachability in POMDPs
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Number of quantifiers is better than number of tape cells
- The complexity of stochastic games
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology
- Infinite games played on finite graphs
- Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
- Code aware resource management
- Synthesizing Protocols for Digital Contract Signing
- Model checking of probabilistic and nondeterministic systems
- Weak Second‐Order Arithmetic and Finite Automata
- Alternating-time temporal logic
- The Büchi Complementation Saga
- Multi-Objective Model Checking of Markov Decision Processes
- Probabilistic Systems with LimSup and LimInf Objectives
- Supervisory Control of a Class of Discrete Event Processes
- AND/OR graph heuristic search methods
- On the menbership problem for functional and multivalued dependencies in relational databases
- An On-Line Edge-Deletion Problem
- Alternation
- The complexity of probabilistic verification
- Trading Performance for Stability in Markov Decision Processes
- Deterministic generators and games for Ltl fragments
- From linear time to branching time
- Computer Science Logic
- Automata-Theoretic Model Checking Revisited
- Measuring and Synthesizing Systems in Probabilistic Environments
- Solving Sequential Conditions by Finite-State Strategies
- Depth-First Search and Linear Graph Algorithms
- Assume-Guarantee Synthesis
- Verification, Model Checking, and Abstract Interpretation
