Graph Games and Reactive Synthesis
From MaRDI portal
Publication:3176385
DOI10.1007/978-3-319-10575-8_27zbMath1392.68233OpenAlexW2803455449MaRDI QIDQ3176385
Roderick Bloem, Krishnendu Chatterjee, Barbara Jobstmann
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_27
Games involving graphs (91A43) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Reactive synthesis from visibly register pushdown automata, Active learning of sequential transducers with side information about the domain, Temporal Logic and Fair Discrete Systems, Combining Model Checking and Deduction, The mu-calculus and Model Checking, Unnamed Item, Quantitative safety and liveness, Subgame optimal strategies in finite concurrent games with prefix-independent objectives, Specifiable robustness in reactive synthesis, OmegaThreads, Church synthesis on register automata over linearly ordered data domains, Unnamed Item, Unnamed Item, Unnamed Item, On Synthesis of Specifications with Arithmetic, Synthesis of Data Word Transducers, Certifying inexpressibility, Unnamed Item, Unnamed Item, Synthesizing adaptive test strategies from temporal logic specifications, Practical synthesis of reactive systems from LTL specifications via parity games, Decoy allocation games on graphs with temporal logic objectives, On Repetition Languages, Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions
Uses Software
Cites Work
- On the Boundary of Behavioral Strategies
- Trading Performance for Stability in Markov Decision Processes
- Solving Partial-Information Stochastic Parity Games
- Deterministic generators and games for Ltl fragments
- Computer Science Logic
- Mathematical Foundations of Computer Science 2004
- Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
- The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies
- Exact algorithms for solving stochastic games
- Markov Decision Processes with Multiple Objectives
- Solving Parity Games in Big Steps
- Automated Technology for Verification and Analysis
- Measuring and Synthesizing Systems in Probabilistic Environments
- Solving Sequential Conditions by Finite-State Strategies
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Automata, Languages and Programming
- Automata, Languages and Programming
- Safraless Compositional Synthesis
- Generalized Parity Games
- Assume-Guarantee Synthesis
- Stochastic Games
- Correct Hardware Design and Verification Methods
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Verification, Model Checking, and Abstract Interpretation
- CONCUR 2003 - Concurrency Theory
- Recursive Concurrent Stochastic Games
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- On the frequency of the transfer paradox
- A survey of stochastic \(\omega \)-regular games
- Finding and fixing faults
- The complexity of stochastic Müller games
- Symbolic bounded synthesis
- Faster algorithms for mean-payoff games
- Assume-guarantee synthesis for digital contract signing
- Alternating finite automata on \(\omega\)-words
- Stochastic limit-average games are in EXPTIME
- Strategy logic
- Automating the addition of fault tolerance with discrete controller synthesis
- Using branching time temporal logic to synthesize synchronization skeletons
- Number of quantifiers is better than number of tape cells
- Positional strategies for mean payoff games
- The complexity of stochastic games
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Reasoning about infinite computations
- The complexity of mean payoff games on graphs
- Energy parity games
- Pushdown processes: Games and model-checking
- Fair simulation
- A survey of partial-observation stochastic parity games
- Strategy synthesis for multi-dimensional quantitative objectives
- Synthesizing robust systems
- Concurrent reachability games
- Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth
- Quantitative Interprocedural Analysis
- Hyperplane Separation Technique for Multidimensional Mean-Payoff Games
- On Stochastic Games with Multiple Objectives
- Multi-objective Discounted Reward Verification in Graphs and MDPs
- Synthesizing Protocols for Digital Contract Signing
- Effective Synthesis of Asynchronous Systems from GR(1) Specifications
- Parameterized Synthesis
- Generalized Mean-payoff and Energy Games
- Qualitative concurrent parity games
- What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives.
- Partial-Observation Stochastic Games: How to Win When Belief Fails
- Mean-Payoff Pushdown Games
- Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy
- Church Synthesis Problem for Noisy Input
- Quantitative Multi-objective Verification for Probabilistic Systems
- On the Complexity of Nash Equilibria and Other Fixed Points
- Temporal Logic and Fair Discrete Systems
- The mu-calculus and Model Checking
- Model Checking Real-Time Systems
- Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
- Introduction to Discrete Event Systems
- Play to Test
- Alternating-time temporal logic
- Bounded Synthesis
- Synthesis for Probabilistic Environments
- An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
- Environment Assumptions for Synthesis
- Infinite Runs in Weighted Timed Automata with Energy Constraints
- A deterministic subexponential algorithm for solving parity games
- The complexity of quantitative concurrent parity games
- Coordination Logic
- Randomness for Free
- Qualitative Analysis of Partially-Observable Markov Decision Processes
- Asynchronous Omega-Regular Games with Partial Information
- Temporal Verification of Reactive Systems: Response
- Synthesis of Asynchronous Systems
- Algorithms for Omega-Regular Games with Imperfect Information
- Inferring Synchronization under Limited Observability
- Multi-Objective Model Checking of Markov Decision Processes
- Better Quality in Synthesis through Quantitative Objectives
- An Antichain Algorithm for LTL Realizability
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Supervisory Control of a Class of Discrete Event Processes
- The Complexity of Markov Decision Processes
- On the menbership problem for functional and multivalued dependencies in relational databases
- The determinacy of Blackwell games
- On the synthesis of strategies in infinite games
- On the synthesis of discrete controllers for timed systems
- Qualitative Determinacy and Decidability of Stochastic Games with Signals
- The Complexity of Partial-Observation Parity Games
- Quantitative solution of omega-regular games380872
- Abstraction-guided synthesis of synchronization
- The theory of deadlock avoidance via discrete control
