However, infinite state spaces occur naturally in domains like software synthesis and cyber-physical systems , and hence handling such games is of great interest. For infinite-state games most problems are directly undecidable. Algorithmic techniques for finite-state two-player games have been studied extensively for many acceptance conditions .
Two-player games are a fundamental model in logic and verification due to their connection to a wide range of topics such as decision procedures, synthesis and control . On multiple benchmark families, our prototype scales dramatically better than previously available tools. We evaluate our prototype implementation on a range of different games.
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. Our approach allows us to infer winning strategies that are structured along the subgoals. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. 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. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. We present a causality-based algorithm for solving two-player reachability games represented by logical constraints.
0 kommentar(er)
