CISPA
Browse
cispa_all_3448.pdf (680.86 kB)

Causality-Based Game Solving

Download (680.86 kB)
conference contribution
posted on 2023-11-29, 18:16 authored by Christel Baier, Norine CoenenNorine Coenen, Bernd FinkbeinerBernd Finkbeiner, Florian Funke, Simon Jantsch, Julian SiberJulian Siber
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.

History

Preferred Citation

Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch and Julian Siber. Causality-Based Game Solving. In: Computer Aided Verification (CAV). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2021-07-20

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3448, title = "Causality-Based Game Solving", author = "Baier, Christel and Coenen, Norine and Finkbeiner, Bernd and Funke, Florian and Jantsch, Simon and Siber, Julian", booktitle="{Computer Aided Verification (CAV)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC