Graph Games and Reactive Synthesis

DOI10.1007/978-3-319-10575-8_27zbMATH Open1392.68233OpenAlexW2803455449MaRDI QIDQ3176385FDOQ3176385

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

Recommendations

• Non-zero sum games for reactive synthesis
• Deterministic graphical games revisited
• Deterministic Graphical Games Revisited
• Automated Technology for Verification and Analysis
• Games on graphs
• Reachability games on automatic graphs
• Game-perfect graphs

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43)

Cites Work

• Assume-Guarantee Synthesis
• Hyperplane Separation Technique for Multidimensional Mean-Payoff Games
• Mathematical Foundations of Computer Science 2004
• Automating the addition of fault tolerance with discrete controller synthesis
• Title not available (Why is that?)
• Partial-observation stochastic games: how to win when belief fails
• Title not available (Why is that?)
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Assume-guarantee synthesis for digital contract signing
• Qualitative concurrent parity games
• Inferring Synchronization under Limited Observability
• Qualitative determinacy and decidability of stochastic games with signals
• The mu-calculus and Model Checking
• Model Checking Real-Time Systems
• Synthesizing protocols for digital contract signing
• Parameterized synthesis
• The complexity of partial-observation parity games
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• Temporal logic and fair discrete systems
• Exact algorithms for solving stochastic games
• Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
• Church synthesis problem for noisy input
• Quantitative interprocedural analysis
• Effective synthesis of asynchronous systems from GR(1) specifications
• Asynchronous \(\omega\)-regular games with partial information
• Mean-payoff pushdown games
• Measuring and synthesizing systems in probabilistic environments
• The complexity of stochastic games
• The complexity of mean payoff games on graphs
• Stochastic Games
• Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
• Alternating-time temporal logic
• The Complexity of Markov Decision Processes
• Title not available (Why is that?)
• Coordination logic
• Title not available (Why is that?)
• A survey of stochastic \(\omega \)-regular games
• The determinacy of Blackwell games
• Decidability of Second-Order Theories and Automata on Infinite Trees
• What is decidable about partially observable Markov decision processes with omega-regular objectives
• On the Complexity of Nash Equilibria and Other Fixed Points
• Introduction to Discrete Event Systems
• Randomness for free
• Qualitative analysis of partially-observable Markov decision processes
• Algorithms for Omega-Regular Games with Imperfect Information
• The complexity of partial-observation stochastic parity games with finite-memory strategies
• Markov Decision Processes with Multiple Objectives
• Concurrent reachability games
• Title not available (Why is that?)
• Supervisory Control of a Class of Discrete Event Processes
• Title not available (Why is that?)
• Title not available (Why is that?)
• Using branching time temporal logic to synthesize synchronization skeletons
• Temporal verification of reactive systems: response
• Positional strategies for mean payoff games
• Reasoning about infinite computations
• Synthesizing robust systems
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Quantitative multi-objective verification for probabilistic systems
• Better Quality in Synthesis through Quantitative Objectives
• Title not available (Why is that?)
• Reasoning about strategies
• Synthesis for Probabilistic Environments
• Environment Assumptions for Synthesis
• Title not available (Why is that?)
• Title not available (Why is that?)
• Alternating finite automata on \(\omega\)-words
• Pushdown processes: Games and model-checking
• A survey of partial-observation stochastic parity games
• On stochastic games with multiple objectives
• Multi-objective discounted reward verification in graphs and MDPs
• Title not available (Why is that?)
• On the synthesis of strategies in infinite games
• On the synthesis of discrete controllers for timed systems
• Quantitative stochastic parity games
• Automata, Languages and Programming
• Title not available (Why is that?)
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Infinite games played on finite graphs
• Title not available (Why is that?)
• Synthesis of Asynchronous Systems
• Multi-Objective Model Checking of Markov Decision Processes
• Title not available (Why is that?)
• Trading performance for stability in Markov decision processes
• Solving Parity Games in Big Steps
• Generalized mean-payoff and energy games
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• On the frequency of the transfer paradox
• On the boundary of behavioral strategies
• Solving partial-information stochastic parity games
• Strategy logic
• Title not available (Why is that?)
• Bounded Synthesis
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Recursive Concurrent Stochastic Games
• A deterministic subexponential algorithm for solving parity games
• Play to Test
• The theory of deadlock avoidance via discrete control
• Title not available (Why is that?)
• Deterministic generators and games for LTL fragments
• The element of surprise in timed games.
• Energy parity games
• Finding and fixing faults
• Automata, Languages and Programming
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Number of quantifiers is better than number of tape cells
• Fair simulation
• Title not available (Why is that?)
• The complexity of quantitative concurrent parity games
• On the menbership problem for functional and multivalued dependencies in relational databases
• The complexity of stochastic Müller games
• Title not available (Why is that?)
• Quantitative solution of \(\omega\)-regular games
• Abstraction-guided synthesis of synchronization
• Computer Science Logic
• Solving Sequential Conditions by Finite-State Strategies
• Generalized Parity Games
• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Stochastic limit-average games are in EXPTIME
• Automated Technology for Verification and Analysis
• An Antichain Algorithm for LTL Realizability
• Safraless Compositional Synthesis
• Symbolic bounded synthesis
• An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
• Faster algorithms for mean-payoff games

Cited In (42)

• On Repetition Languages
• A game-theoretic approach for the synthesis of complex systems
• Certifying inexpressibility
• Practical synthesis of reactive systems from LTL specifications via parity games
• Active learning of sequential transducers with side information about the domain
• From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
• Synthesis of data word transducers
• Church synthesis on register automata over linearly ordered data domains
• Reactive synthesis from visibly register pushdown automata
• Games where you can play optimally with arena-independent finite memory
• Half-positional objectives recognized by deterministic Büchi automata
• Non-zero sum games for reactive synthesis
• Graph games and logic design
• A game-theoretic approach to indistinguishability of winning objectives as user privacy
• Temporal logic and fair discrete systems
• Computer aided synthesis: a game-theoretic approach
• The mu-calculus and Model Checking
• Title not available (Why is that?)
• Specifiable robustness in reactive synthesis
• Quantitative reachability Stackelberg-Pareto synthesis is \textsf{NEXPTIME}-complete
• Synthesising features by games
• Synthesis with privacy against an observer
• Using the compatibility analysis of logical specifications of automata to solve game problems
• Decoy allocation games on graphs with temporal logic objectives
• Quantitative safety and liveness
• Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions
• Different strokes in randomised strategies: revisiting Kuhn's theorem under finite-memory assumptions
• Synthesis of Data Word Transducers
• Stackelberg-Pareto synthesis
• Adapting to the behavior of environments with bounded memory
• Combining Model Checking and Deduction
• Strategy representation by decision trees in reactive synthesis
• Subgame optimal strategies in finite concurrent games with prefix-independent objectives
• On synthesis of specifications with arithmetic
• Title not available (Why is that?)
• LTL reactive synthesis with a few hints
• Energy mean-payoff games
• Title not available (Why is that?)
• OmegaThreads
• Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs
• Infinite separation between general and chromatic memory
• Synthesizing adaptive test strategies from temporal logic specifications

Uses Software

• MCGP
• CUDD
• UMDES
• LTL2BA

This page was built for publication: Graph Games and Reactive Synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176385)