In order to guarantee these games to be smaller, we solve the post-game under the assumption that the considered subgoal was bridged for the last time. We slice the game along a necessary subgoal into two parts, the pre-game and the post-game. This motivates the following recursive approach. In contrast, determining whether a subgoal is sufficient requires a partial solution of the given game. We show how Craig interpolants can be used to compute necessary subgoals, making our methods applicable to games represented by any logic that supports interpolation. The two properties differ in one key aspect: While necessity of a subgoal only considers the paths of the game arena, for sufficiency the game structure is crucial. Dual to the description in the preceding paragraph, sufficient subgoals provide a chance for the reachability player to win the global game as they must merely reach this intermediate target. We call a subgoal sufficient if indeed the reachability player has a winning strategy from every state satisfying the post-condition of the subgoal. On the other hand, passing through a necessary subgoal is in general not enough for the reachability player to win. Finding such a necessary subgoal may let us conclude that the safety player wins without ever having to unroll the transition relation. Thus for the safety player, a necessary subgoal provides a chance to win the game based on local information: If they control all states satisfying the pre-condition of the subgoal, then any strategy that in these states picks a transition outside of the subgoal is winning. Subgoals open up game solving to the study of cause-effect relationships in the form of counterfactual reasoning : If a cause (the subgoal) had not occurred, then the effect (reaching the goal) would not have happened. It represents an intermediate target that the reachability player must reach in order to win. A necessary subgoal is a transition predicate that is satisfied at least once on every play that reaches the overall goal. In this paper, we present a novel technique for solving logically represented reachability games based on the notion of subgoals. While is based on automated theorem-proving for Horn formulas and handles a wide class of acceptance conditions, the work in focusses on reachability games specified in the theory of linear arithmetic, and uses sophisticated decision procedures for that theory. More recently, incomplete procedures for solving infinite-state two-player games specified using logical constraints were studied . The authors assume a symbolic encoding of the game in a very general form. An elegant classification of infinite-state games that can be algorithmically handled, depending on the acceptance condition of the game, was given in . 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 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |