Causality-Based Game Solving

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributed

Contributors

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.

Details

Original languageEnglish
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan M. Leino
PublisherSpringer, Berlin [u. a.]
Pages894–917
Number of pages24
ISBN (electronic)978-3-030-81685-8
ISBN (print)978-3-030-81684-1
Publication statusPublished - 15 Jul 2021
Peer-reviewedNo

Publication series

SeriesLecture Notes in Computer Science, Volume 12759
ISSN0302-9743

Conference

Title33rd International Conference on Computer-Aided Verification
Abbreviated titleCAV 2021
Duration18 - 24 July 2021
Website
Degree of recognitionInternational event
Locationonline

External IDs

ORCID /0000-0002-5321-9343/work/142236693
Scopus 85113493549

Keywords

Library keywords