Causality-based game solving

DOI10.1007/978-3-030-81685-8_42MaRDI QIDQ832242zbMATH OpenOpenAlexFDO

Authors Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, Julian Siber

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2105.14247

Mathematics Subject Classification ID

Applications of game theory (91A80) 2-person games (91A05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to reach the goal. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. Our approach allows us to infer winning strategies that are structured along the subgoals. If the game is won by the reachability player, this is a strategy that progresses through the subgoals towards the final goal; if the game is won by the safety player, it is a permissive strategy that completely avoids a single subgoal. We evaluate our prototype implementation on a range of different games. On multiple benchmark families, our prototype scales dramatically better than previously available tools.

Recommendations

• A constraint-based approach to solving games on infinite graphs
• Solving games via three-valued abstraction refinement
• Reachability games on automatic graphs
• Symbolic computational techniques for solving games
• Synthesising Succinct Strategies in Safety and Reachability Games

Cites work

• scientific article; zbMATH DE number 1863183 (Why is no real title available?)
• scientific article; zbMATH DE number 2243372 (Why is no real title available?)
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• A constraint-based approach to solving games on infinite graphs
• A new solution of Dijkstra's concurrent programming problem
• Automata, logics, and infinite games. A guide to current research
• Causality-based verification of multi-threaded programs
• Compositional synthesis of reactive controllers for multi-agent systems
• Guiding Craig interpolation with domain-specific abstractions
• Handbook of modal logic
• Modal μ-Calculus and Alternating Tree Automata
• On the synthesis of strategies in infinite games
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• Slicing Abstractions
• Synthesis of Reactive(1) designs
• The MathSAT5 SMT solver
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(11)

• Realizability modulo theories
• Software Verification of Hyperproperties Beyond k-Safety
• Counterfactuals modulo temporal logics
• From verification to causality-based explications (invited talk)
• Operational causality -- necessarily sufficient and sufficiently necessary
• Temporal causality in reactive systems
• Logic Programming and Nonmonotonic Reasoning
• Cobra: a tool for solving general deductive games
• Predicate abstraction for hyperliveness verification
• Conflict-aware active automata learning
• Counterfactual causality for reachability and safety based on distance functions

Describes a project that uses

Uses Software

• PySMT
• MathSAT5
• z3

This page was built for publication: Causality-based game solving

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