Causal Solving of Reachability Games
Julian Siber
Two-player games are an elegant way of modeling many problems such as synthesis, which requires constructing a correct system implementation from a formal specification. The specification is encoded in a game between the system and a non-cooperative environment. If a correct implementation for the specification exists, solving the game will yield a system strategy that describes it. However, many practically relevant synthesis applications require solving games over infinite graphs. This remains a particularly challenging problem. In this thesis, we propose a causal technique for solving reachability games represented by logical constraints. We consider games over both finite and infinite graphs. Our method focuses on the cause-effect-relationships of events that need to appear in any play reaching the goal states. To describe the set of possible causes for some effect observed in every such play, we introduce the notion of subgoals for two-player games. Subgoals provide a way to determine that the safety player wins using counterfactual reasoning: If they avoid all possible causes described by the subgoal, then the effect of reaching the goal states cannot happen. Using this, we may infer a winning safety player strategy based on a small number of key decisions without fully computing the winning regions of both players. Dual to this, we can determine that the reachability player wins by finding a sequence of subgoals that connects some initial state to the goal states. We implemented a prototype tool called CabPy and evaluated it on a variety of games over both finite and infinite graphs. The evaluation demonstrates that our approach works well in practice. Compared to SimSynth, a state-of-the-art tool for solving reachability games over infinite graphs, CabPy scales considerably better on several benchmark families.
Master Thesis.