The Game Description Language (GDL) is a lightweight formalism for representing the rules of arbitrary finite perfect information games. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Coalition Logic (CL) is a logical framework capable of expressing strategic behaviors of a set of players that involve finitely many successive game states, which can formulate important properties such as whether one player can enforce a win of the game within a certain number of steps, regardless of the actions of the other players. In this paper, we investigate how to define the CL model-checking problem in the context of GGP and how to reason about CL properties of general games using Quantified Boolean Formula (QBF) solvers. This work extends our earlier AAMAS 2024 paper [1]. We evaluate the eficiency of our approach through a case study involving two-player general games and show that it has the potential to assist general game-playing agents with endgame analysis.
The Game Description Language (GDL) is a lightweight knowledge representation formalism for describing the rules of arbitrary games [2]. GDL describes game rules in normal logic program syntax similar to Prolog. It is used as the input language for general game-playing (GGP) systems, which can learn to play any new game from its rules alone and without human intervention, thereby demonstrating a form of general intelligence. As a lightweight specification language, GDL merely provides means for representing the rules of a game. At the same time, a crucial aspect of GGP is the ability to automatically reason about a given specification. In early years, successful GGP systems performed random simulations to test the validity of certain properties and rely on their informed guess in case no violation could be detected [3]. However, validating properties through random simulations can be unreliable, and the performance of the GGP system can be afected if incorrect assumptions are made about the game.
techniques have been introduced to support GGP systems in formally analyzing whether a GDL description satisfies certain logical properties. Notable work in this area include using the modelchecker Mocha to reason about properties of GDL games specified in Alternating-time Temporal logic (ATL) [4] and using Answer Set Programming to reason about General Game Temporal Logic (GTL) properties–a logic similar to the Linear Temporal Logic with only the temporal operator “next”– of GDL games [5]. However, model-checking against ATL typically requires expanding all game states to construct the underlying Concurrent Game Structure, which is only practical for very small games. While model-checking against GTL has much lower computational complexity and does not require explicitly storing all game states in memory, GTL cannot express any strategic properties. Hence, it is interesting to investigate whether there is some logical framework that can express strategic properties of general games, and whose model-checker has the potential to be used by GGP systems in practice.
Coalition Logic (CL) [6], a logical fragment of ATL that includes only the temporal operator “next,” can express strategic behaviors of groups of players over finitely many successive game states. For instance, it can capture important solution concepts such as bounded-depth strong winnability, which asks whether a player can enforce a win within a certain number of steps, regardless of the actions of
CEUR
ceur-ws.org the other players. Importantly, model checking for CL has significantly lower computational complexity than for ATL, making it a more practical choice for use in GGP systems.
approach to reasoning about CL properties of GDL games. To this end, we define the syntax and semantics of CL for general games (GCL). We present the complexity of GCL model-checking and show how some important game properties of GDL games can be formulated with GCL. We present a sound and complete method of GCL model-checking leveraging Quantified Boolean Formula (QBF) solvers [ 7].
Our work is related to the QBF-based approach of reasoning about bounded-depth strong winnability of specific
perfect information games such as Generalized Tic-Tac-Toe and Hex [8]. Such an approach usually involves encoding the bounded-depth strong winnability of some specific strategic games with QBF based on human interpretation of the game rules and calling a QBF solver to evaluate the expression. It has been shown in Generalized Tic-Tac-Toe that QBF solvers can prove bounded-depth strong winnability faster than proof number search solvers [9]. Since bounded-depth strong winnability is just one property that can be expressed in GCL, and GDL can express all finite perfect information games, our work is a generalization of existing literature.
We assume readers to be familiar with basic concepts of logic programming with negation, Answer Set
The Game Description Language (GDL) can be used to describe the rules of any finite game with concurrent moves. GDL uses a normal logic program syntax along with the following preserved keywords used to describe the diferent elements of a game [ 2]: role() base( ) input(, ) init( ) true( ) legal(, ) does(, ) next( ) terminal goal(, )
is a player is a base proposition for game positions Action is in the move domain of player base proposition holds in the initial position base proposition holds in the current position can do move in the current position
player does move holds in the next position the current position is terminal gets points in the current position There are further restrictions for a set of GDL rules to be valid [2]: role can appear only in facts; init and next can only appear as heads of rules; true and does can only appear in rule bodies. Moreover, init cannot depend on true, does, legal, next, terminal, or goal while legal, terminal, and goal cannot depend on does. Finally, valid game descriptions must be stratified and allowed—such logic programs always admit a finite grounding and a unique stable model.
A valid GDL game description over ground terms Σ can be interpreted as a multi-agent state transition system: Let = { ∈ Σ | ⊧ ( )}
be the base propositions and = {(, ) ∈ Σ × Σ | ⊧ (, )} and = { the move domain for the players. Suppose that = { 1, ... , } ⊆ is any given position 1, ... , } → Σ any function that assigns to each of ≥ 1 players an action from their move domain. In order to use the game rules to determine the state update, needs to be encoded as a set of facts using keyword true:
= { ( keyword does: = {( 1, ( 1))., ..., (
, ( )).}. 1)., ... , ( ).} and the joint action by a set of facts using Definition 1 ([11]). The semantics of a valid GDL description is the transition system (,
role()} (player names) • 0 = { ∈ | ⊧ • = { ⊆ | ∪ • = {(, , ) | ∪ • (, ) = { ∈ | ∪ • = {(, , ) | ∪ init( )} (initial state) ⊧ terminal} (terminal states) ⊧ legal(, )} (legal moves) ∪
⊧ next( )} (update) ⊧ goal(, )
and ∈ ℕ and 0 ≤ ≤ 100} (goal value)
0 −−→1 1 −−→ ... −1 2 −−→ In the above game sequence, we write −−−+→1 +1 if ∉ and all moves are legal in the state in which they are taken, that is, ( , +1 ( ), ) ∈ for each ∈ . We say a valid game playing sequence terminates in steps if ∈ [5].
Similar to the diference between QBF and SAT [ 12], allowing quantifiers in ASP programs can provide a more expressive language. The resulting language is called Quantified Answer Set Programming (QASP). Its semantics is defined as follows.
Definition 2 ([13]). Let be a logic program with ground atoms A. A QASP over A has the form 1 1 ... where are pairwise disjoint subsets of A, every is either ∃ or ∀, and is a logic program over A. We define fix ( , ) , where ⊆ ⊆ A, as the logic program: {:- . | ∈ } ∪ { :- . | ∈ \ }.
A normal logic program P is satisfiable if it has a stable model. Satisfiability of a QASP is recursively defined as follows.
1. If the QASP has form ∃ (resp. ∀ ), the program is satisfiable if there exists (resp. for all) ⊆ such that the program ∪ fix ( , ) is satisfiable. 2. If the QASP has form ∃ Q (resp. ∀ Q ), the program is satisfiable if there exists (resp. for all) ⊆ such that the program Q ( ∪ ( , )) is satisfiable.
QASP has the same expressive power as QBF. A QASP can be solved by converting it to an equalsatisfiable QBF expression using tools like qasp2qbf [13] and calling a QBF solver to evaluate the satisfiability of the converted expression. 3. Coalition Logic For General Games
Definition 3 (GCL Syntax). The Coalition Logic for General Games is defined over a valid GDL description that has the following grammar: ∶∶= ∣ ∧ ∣ ¬ ∣ ⟨⟨⟩⟩
X where is a ground atom of that is not an instance of the predicate symbol init, next and does not depend on does. is a subset of players in (i.e., ⊆ ). Standard propositional operators ∨ and → are also allowed and defined as usual.
traces [14], with only the primitive temporal operator ⟨⟨⟩⟩ X (read “the current state is non-terminal and the players in can enforce to hold next”). We introduce the abbreviation [[]] X̃¬ ∶∶= ¬⟨⟨⟩⟩ X (read “the current state is terminal or no matter what the players in do, players in ∖ have a set of legal joint moves to ensure does not hold next”).
For a GDL description and any subset of players = { 1, … , || } ( ⊆ ), we define the notation (, ) = {{( 1, 1)., … , ( || , || ).} ∣ ∀ ∈ , ∪ ⊧ ( , )}, which denotes the set of all possible legal joint actions of players in a coalition at state . The semantics of GCL is given as follows.
Definition 4 (GCL Semantics). Let be a valid GDL description, and is a GCL formula over . Then, we say satisfies at (written , ⊧ ) as per the following inductive definition: , ⊧ , ⊧ ¬ , ⊧ 1 ∧ 2 , ⊧ ⟨⟨⟩⟩ X if if if if ∪ , ⊧ ̸
⊧ ( ) , ⊧ 1 and , ⊧ ∪
⊧ ̸ where ′ = { ∈ ∣ ∪
2 and ∃ ∈ (, ).
such that ∀ ∈ ( ∖ , ). ,
′ ⊧ ∪ ∪ ⊧ ( )}
For a GDL description and a formula , the GCL model-checking task decides if , 0 ⊧ holds, which is abbreviated as ⊧ .
GTL, GCL can express non-strategic properties that involve finitely many successive game states. For example, universal termination within steps can be expressed as follows.
• () ≡ (0) ∨ [[]]
X̃ ( − 1) , where (0) ≡ .
Turn-taking is another important non-strategic property, which requires that at every step of the game, exactly one player is allowed to take a turn—i.e., has more than one legal action. For games that are guaranteed to terminate within steps, this property can be expressed using the following GCL formula. • () ≡ (0) ∧ [[]] • ( ) ≡ ⋁(,)∈ ∧(,)∈ ∧≠
X̃ ( − 1) , where (0) ≡ ¬ ⋁ ∈∧ ∈∧ ≠ ( ( ) ∧ ( )), and ( , ) ∧ ( , ) (recall that is the move domain of all players)
Besides non-strategic properties, GCL can also formulate strategic properties. A general game player might be concerned about whether it can win the game within steps (aka. bounded-depth strong winnability) regardless of the actions of the remaining players. This can be expressed as follows: • (, ) ≡ (, 0) ∨ ⟨⟨{}⟩⟩
X (, − 1) , where (, 0) ≡ (, 100) ∧ .
The existence of a threatening move is another interesting strategic property. In a two-player turn-taking
game, if the players take alternating moves (i.e., one player might have more than 1 legal action in odd
steps and the other player might have more than 1 legal action in even steps), then, we say that a player
that is taking turn has a threatening move if there exists a legal action for in the current state such
that, in the next state, the opponent has at most one legal response that prevents from winning the
game within steps (for some small value of ). For example, in Tic-Tac-Toe, player has a threatening
move in step 1 by marking the corner-cell (
• ((, ))
:- (, ).
• ℎ (, ) ≡ ⟨⟨{}⟩⟩
X(
(, 0) ∨ (, )) , where • (, ) ≡ ⋀(,),(,)∈ ∧≠
(, , ) ∨ • (, , ) ≡ [[]]
X̃¬ ((, )) ∨
(, ) (, , ) , Here, (, , ) checks that for all legal moves of player , either does not perform action or player can force a win within steps. In other words, (, , ) does not hold if and only if player can play action to ensure that cannot force a win within steps. (, ) ensures that every pair of actions and in the move domain of , either (, , ) or (, , ) hold. This means that has at most 1 legal action in the next state to ensure that cannot enforce a win within steps. We end this section by stating the complexity result of GCL model-checking. Theorem 1. GCL model-checking over a ground GDL description and a formula is PSPACE-complete. Proof. GCL model-checking is in PSPACE because one can perform model-checking by following the semantics definition 4, and the trivial recursive algorithm uses a polynomial amount of space. The hardness result is based on the fact that verifying bounded-depth strong winnability for two-player games when the depth is encoded in unary is PSPACE-hard [15].
Readers familiar with CL might wonder why the complexity of model-checking against a ground GDL description is PSPACE instead of PTIME when applied to Concurrent Game Structures. This is because GDL can represent game models that are exponentially larger than the size of the GDL description. 4. QASP Encoding for GCL Model-Checking One can perform GCL model-checking naively by following its semantics definition; however, it is ineficient (see Section 5 for more details). Due to the PSPACE-completeness of GCL model-checking, using a QBF solver to perform the task is a viable option. We now discuss how to perform GCL model-checking with QBF solvers. GDL and QASP utilize stable models for their semantics, whereas QBF is based on classical models. Encoding the GCL model-checking task in QBF directly is therefore challenging as it would require some form of completion technique [16]. Thanks to work on converting from QASP to QBF [13], dealing with the completion task from scratch is unnecessary as long as we can encode GCL model-checking in QASP.
To perform GCL model-checking expressions with QASP, we need to convert the GCL formula into negation normal form (NNF), where the negation symbol only appears in front of ground atoms of (i.e., we substitute ¬ in Definition 9 with ¬ ). The only other allowed operators are ∨, ∧, [[]] X̃, and ⟨⟨⟩⟩ X. The procedure of rewriting GCL formulas to NNF is similar to rewriting other modal logics to NNF, which is based on the elimination of →, the definition of [[]] X̃, and the use of De Morgan’s laws [17]. Similar to other modal logics, if the input GCL only contains the operators ¬, ∨, ∧, →, ⟨⟨⟩⟩ X, and [[]] X̃, we can ensure that the converted NNF has at most a linear growth in the formula size [17].
Based on the semantics of GCL, we know that whether ⊧ depends on the truth value of each of the subformulas of at diferent states of . We now introduce the concept of subformula positions, which is a mapping from subformulas of to their unique operator prefix in the syntax tree. Definition 5 (Subformula Position). Given a GCL formula , the position of each subformula in (denoted as ( ) ) is recursively defined as follows: • If (¬ ) = • If ( , then ( ) = ¬
(similarly for [[]] X̃ and ⟨⟨⟩⟩ X). 1 ∧ 2) = , then ( 1) = ∧ 1 and ( 2) = ∧ 2 (similarly for 1 ∨ 2).
We define () =
and denote as the set of all positions of all subformulas of . • ( • (⟨⟨{}⟩⟩ 1) = , and 1() = 0
value of diferent subformulas in might be evaluated at the same state of . We provide a name to each position of so that two subformulas have the same position naming if and only if they are within the same scope of ⟨⟨⟩⟩ X and [[]] X̃, and as a result, their truth value are always evaluated at the same state of . Our notion of subformula positions and position naming is inspired by similar concepts used in epistemic GTL model-checking [18].
Definition 6 (Position Naming). Let be a valid GDL description and a GCL formula. A position naming for is a function ∶ → ℕ such that () = 0 ; and for all positions 1, 2 ∈ and their longest prefixes 1′ and 2′ which ends in some ⟨⟨⟩⟩ X or [[]] X̃ we have that ( 1) = ( 2) if 1′ = 2′ (where ′ = if no such ⟨⟨⟩⟩ X or [[]] X̃ exists).
We define the depth of a position name ( ) (denoted as ℎ( ( )) ) as the total number of ⟨⟨⟩⟩ X or [[]] X̃ operators in . The degree of a GCL expression (denoted as () ) is the maximum possible depth of any position name ( ) such that ∈ , which is also equal to the maximum nesting of ⟨⟨⟩⟩ X or [[]] X̃ operators in the syntax tree of .
Example 1. Consider the formula 1 = (⟨⟨{}⟩⟩ X (, 100)∧ )∨([[{}]] X̃ (, 100)∧ ) , which says that either can force a win in the next state or no matter what does, can let win in the next state. The positions of the subformulas of 1 and a possible valid position naming is as follows: • (
2) = ∨ 2 [[{}]] X̃∧2, and 1( ∨ 2 [[{}]] X̃∧2) = 2 Although appears twice in 1, they are diferent subformulas of 1. For clarity, we use 1 and 2 to distinguish them. The position naming above ensures that any subformulas within the same scope of the temporal operator have the same naming. For example, when performing GCL modelchecking against 1, we know that (, 100) and 2 should always be evaluated at the same state to decide the truth value of the subformula (, 100) ∧ 2, thus, they should have the same position naming. For the valid position naming provided in this example, we can ensure this requirement because the subformulas (, 100) , 2, and (, 100) ∧ 2 all have the same position naming 2.
The depth of the position names is given as: ℎ(0) = 0 and ℎ(
of depends on the evaluation of all subformulas ′ of that have the same position name as at state and the evaluation of all subformulas ″ that have exactly 1 more nesting of temporal operators at some successor state ′ of . We now introduce the concept of successor position, which refers to all positions that have exactly 1 more nesting of the temporal operators than the current position.
1) = ∨ 1 ⟨⟨{}⟩⟩ X∧2, and 1( ∨ 1 ⟨⟨{}⟩⟩ X∧2) = 1
1) = ∨ 1, and 1(∨ 1) = 0 1) = ∨ 1 ⟨⟨{}⟩⟩ X, and 1( ∨ 1 ⟨⟨{}⟩⟩ X) = 1 1 ⟨⟨{}⟩⟩ X∧1, and 1( ∨ 1 ⟨⟨{}⟩⟩ X∧1) = 1
2) = ∨ 2, and 1(∨ 2) = 0 2) = ∨ 2 [[{}]] X̃, and 1( ∨ 2 [[{}]] X̃) = 2 2 [[{}]] X̃∧1, and 1( ∨ 2 [[{}]] X̃∧1) = 2 ⟨⟨⟩⟩ X or [[]] X̃ we have that 1′ is a proper prefix of 2′.
Definition 7 (Successor Position Name). Suppose that is a valid GDL description, is a GCL formula, 1 and 2 are two positions in , and ∶
→ ℕ is a valid position naming function. A position name ( 2) is a successor of the position name ( 1) (denoted as ( ( 1), ( 2))) if and only if ℎ( ( 2)) = ℎ(
( 1)) + 1, and for the longest prefixes 1′ of 1 and 2′ of 2 which ends in some
Example 2. Consider the formula 1 = (⟨⟨{}⟩⟩
with the same position naming as in Example 1. Then, both position names 1 and 2 are successor positions
of the position name 0 (i.e., (
). This implies that the truth value of 1 with position name 0 may depend on the evaluation of the subformulas of 1 with position names 1 and 2. ultimate goal is to ensure that ⊧ if and only if the QASP is satisfiable.
similar to the method discussed in GTL model-checking [5].
Definition 8 (Position Extension). Suppose is a valid GDL description, the Position-Extended ASP of (denoted as () ) is obtained from as follows: • Change all occurrences of ( ) to ( , ( , 0)) and all occurrences of ( ) to ( , (, 0)) . #» #» depends on does, change it to ( , (, 1)) .
∉ { , } • For any atom of the form ( ) (i.e., predicate with argument ) such that the pre#»dicate symbol ; if depends on #t»rue but does not depend on does, change it to ( , ( , 0)) ; if • For each rule whose head has been extended by ( , 0) , add ( ) to its body; and for each rule whose head has been extended by (, 0) or (, 1) , add ( , ) to its body.
We extend the definition of to () = { ( , (, 0)) ∣ ( ) ∈ } and the definition of to () = {( 1, ( 1), (, 1)), ..., ( , ( ), (, 1))} Example 3. Consider the following rule of Tic-Tac-Toe, which says that if player marks a cell and the cell is currently blank, the cell will be marked as in the next state.
• ( ( , , )) ∶ − ( ( , , )), (, ( , )).
In () , the rule is mapped to
• ( ( , , ), (, 0)) ∶ − ( ( , , ), ( , 0)), (, ( , ), (, 1)), ( , ).
Note that the program () is stratified whenever is. The following theorem shows the semantics equivalence of () and valid game playing sequences in the original game description . Theorem 2. Consider a GDL description G with semantics (, (0 ≤ ≤ ) are arbitrary pairwise distinct integers. Then, for any predicate symbol in the game description and for all 0 ≤ ≤ , such that is not init or next and does not depend on does, we have: • = { | ⊧ ( , ( • ∪
#» ⊧ ( ) if ⊧ ( , ( , 0)) , 0))}, and
#» In particular, since does not depend on , ∪ ⊧ ( , ) if ⊧ ( , , ( , 0)).
that in [5], it assumes that = .
Next, we show how a GCL formula can be encoded as an ASP program. Similar to GTL modelchecking [5], we assume that there is a function ( , ) that would give an atom of arity 0 for each GCL formula with position naming .
Definition 9. Suppose that is a GCL formula in NNF, the ASP encoding of any of its subformula with position (denoted as ( , ( )) ) is recursively defined as follows:
#» #» #» • (( ), ) = {(( ), ) :- ( , (, 0)).} .
#» #» #» • (¬( ), ) = {(¬( ), ) :- ( , (, 0)).} . • ( • ( • (⟨⟨⟩⟩
The intuition of the above inductive encoding is as follows. Suppose that we want to evaluate the subformula with#»position at state , the atom ( , ) holds if a#»nd only if , ⊧ . Th#»e case when is a ground atom ( ) is converted to a rule which justifies (( ), ) if and only if ( ) with position holds at state . To show that where = 1 ∧ 2 holds (i.e., ( 1 ∧ 2, ) is justified), the encoding states that the both subformulas 1 and 2 must be justified at state . Remark that the positions ∧ 1 and ∧ 2 have the same name, because they are within the same scope of ⟨⟨⟩⟩ X and [[]] X̃. with connectivities ¬ or ∨ are defined the same way as in the GTL model-checking encoding [ 5].
The case when the subformula is of the form ⟨⟨⟩⟩ X with position naming ( ) is converted to rules which justify (⟨⟨⟩⟩ X, ( )) if and only if the current state is not terminal and the players joint actions of the players perform at would lead us to a successor state ′ such that the formula with position ( ⟨⟨⟩⟩ X) holds at ′. The case when the subformula is of the form [[]] X̃ with position naming ( ) is converted to rules which justify ([[]] X̃, ( )) if and only if the current state is terminal or the players joint actions of the players perform at would lead us to a successor state ′ such that the formula with position ([[]] X̃) holds at ′.
In the last two cases, whether a subformula at a state holds is related to the joint actions of the players and whether holds in the successor state ′ of . Similar to GTL model-checking [5], we need an action generator program in ASP. Suppose that the current state is and we want to reason about a subformula with position name whose truth value is related to the truth value of the subformula at position name at some successor state ′ of such that (, ) holds. The action generator program describes the state transition from to ′ (cf. Theorem 2), which generates 1 action per player that is legal at state as long as cannot be derived at position name . Since GCL also involves existential and universal quantification of player actions at a particular state, we define the following action generator, which generates 1 action per player that is legal at state such that one successor of position name is position and the actions of the players in are quantified existentially (i.e., the subformula is of the form ⟨⟨⟩⟩ X ), while the actions of the players in ∖ are quantified universally. Definition 10 (Action Generator). Suppose that is a valid GDL description, ⊆ is a coalition, and the names of two positions, the action generator (, , , ) contains the following clauses. 1. ((, 0)) 2. ((, 0)) :- ((, 0)).
:- ((, 0)). 3. 1 {(, , (, 1)) ∶ (, )} 1 4. :- (, , (, 0)), (, , (, 1)).
:- ((, 0)), (). 5. For each ∈ ∖ , create the clause: { ( , , (, 1)) ∶ ( , )}
and each in the move domain of , create the clause: ( , , (, 1)) :- ( , ( , , (, 0)), ((, 0)), ( , 1, (, 1)), … , ( , , (, 1)).
1, (, 1)), … , ( , , (, 1)), where 1, … , are the 1 bits in the binary representation of − 1 , and 1, … , are the 0 bits in the binary representation of − 1 . players in ∖
In the action generator, (
) at a particular state. We need to ensure that every player in this set must make
exactly one legal action. Note that we cannot simply use integrity constraints like (
rules of the form (
might be less than 2|| , which means there might be some binary that do not correspond to a legal action in the move domain. In this case, no
can be generated by rule (
is generated in such a case.
Example 4. Consider the formula 1 = (⟨⟨{}⟩⟩ with the same position naming as in Example 1. Then, one possible definition of the mapping of the
1, 0) the GCL formula 1 contains the following clauses: • 0 :- 1. • 1 :- 2, ((0, 0)).
• The action generation programs: (, {}, 0, 1)
and
• Facts: (
(
(
(
(, {}, 0, 2)
_(, 1)
must be justified. Hence, we add the integrity constraint {:- (, 0)}
to our encoding. Note that all encodings we have discussed so far do not involve any actual quantification. To verify a GCL formula, we need to define a quantifier prefix Q to the program (, 0) ∪ {(0).} ∪ if and only if ⊧ . The idea is to quantify all ground atoms of the predicate program universally, and all the other ground atoms existentially. One possible quantification method based on atom dependency is defined as follows, which is similar to the method we discussed in [ 1]. in the ground Definition 11 (Atom dependency). Suppose that is an ASP program with grounding A and is the ground normal logic program of . For two atoms , ∈ A we say that depends on in if the following recursive definition holds: Program contains a rule such that the atom appears in the head of the rule and the atom appears in the body of the rule; or, there exists an atom ∈ A such that depends on and depends on . We denote that depends on by → .
Definition 12 (Dependency Based Quantification Method) . Suppose A is the set of ground atoms of the program is of form where program = (0) ∪ (, 0) ∪ {(0).} ∪ 0 = ()
A, the quantifier block it belongs to is determined by the following three rules: 1. If = ( , , (, 1)) 2. If = ( , , (, 1)) 3. If = ( , , (, 1)) for some , , then ∈ ℎ() 4. Otherwise, ∈ with the maximum 1 ≤ ≤ such that ( , , (, 1)) → ( , , (, 1)) ∈
A and ℎ() = . If no such exists then ∈ 0
To put it in words, we quantify the ground atoms of that is an instance of the predicate universally. Item 1 ensures that the quantification level of the universal variables follows the depth of the position names. There are two possible situations of the quantifier level of a ground atom that is an instance of and is extended with position name (e.g., ( , , (, 1)) ). We should note that the action generator generates any instance of in the program . To generate the ground atom ( , , (, 1)) in , the program
(, , , ) . According to definition 9, (, , , ) must be part of (, 0)
for some (, ) is part of (, 0) if and only if either (⟨⟨⟩⟩ ([[ ∖ ]] ( , , (, 1))
X, ) is part of (, 0)
. For the former case, we want to verify whether ⟨⟨⟩⟩ X̃ holds.
The actions of players in should be generated before the actions in ∖ . Therefore, in item 2, if ∈ , should be quantified existentially in ℎ()−1 . In all other cases, according to item 3, the ground atom ( , , (, 1)) should be quantified existentially in ℎ()+1 . Item 4 ensures that no ground atom in that depends on an action is quantified before that action atom.
X, ( )) at state , must not be terminal and (, ( ⟨⟨⟩⟩
justified at the successor state. With our quantification method, we can ensure that (⟨⟨⟩⟩
X,
( ))
is justified if and only if the is not terminal and there exists some legal joint actions of the players
for some
X̃, )
and
or
in such that for all legal joint actions of players in ∖ , (, ( ⟨⟨⟩⟩ X)) must be justified in the
successor state and thereby shows that , ⊧ ⟨⟨⟩⟩ X . Generating all legal joint actions of players in
∖ is achieved by the logarithmic encoding of the actions of the players in ∖ .
Example 5. Consider the formula 1 = (⟨⟨{}⟩⟩ X (, 100)∧ )∨([[{}]] X̃ (, 100)∧ )
with the same position naming as in Example 1. Let = 0 (0) ∪ (, 0) ∪ {(0).} ∪ () ∪
{:- (, 0)} and the quantifier prefix Q and the ground atoms of is A. Assume the move domain of
players is {(, 1), (, 2), (, 3), (, 1), (, 2), (, 3)}. Then, the quantifier prefix of has the form
∃ 0∀ 1∃ 1, where:
• 0 = { ((0, 0)), (0..2), (
In QBF research, “quantification method” is also referred to as “prenexing strategy”. For GCL
modelchecking, there are many correct prenexing strategies. For example, due to both (, 0) and ()
are stratified, the quantifier prefix of can also be defined as follows, where 0′ = {(, , (
Diferent prenexing strategies can significantly afect the eficiency of GCL model-checking [ 1]. Systematically exploring how the eficiency of GCL model-checking can be afected by diferent prenexing strategies is beyond the scope of this paper. Interested readers can find out more about how prenexing strategies can afect the eficiency of QBF solving in [ 19].
of a logarithmic encoding to handle the existential and universal quantification over players’ actions. The following proposition states the correctness of the encoding, which can be proved by induction on the structure of the GCL formula (cf. our explanation in Definition 9) and relies on Theorem 2 1. Proposition 1. Suppose that is a valid GDL description and is a GCL formula over , then ⊧ if and only if the following QASP is satisfiable.
Q 0 (0) ∪ (, 0) ∪ {(0).} ∪
One of the most important strategic properties of games is strong winnability, which is whether a player has a strategy to win the game regardless of the actions of the remaining players. In this section, we briefly report the eficiency of our QBF-based model-checking method on reasoning strong winnability on some popular turn-based two-player games: Generalized 4×4 Tic-Tac-Toe (GT-1-1, and GT-2-2) [9], Connect-3 (C-3), Connect-4 (C-4) [20], Breakthrough (BT) [21], and Dots and Boxes (D&B) [22]. For 1Detailed proof is available here: https://github.com/hharryyf/gdl2qbf-general
GDL description & GCL formula in NNF encode translate solve simplicity, we assume the two players in these games are denoted as and , with as the player taking the first turn. We only concern ourselves with whether the game is strongly winnable by player . We test the eficiency of our model-checking method on various game configurations. For C-3, C-4, BT, and
the strong winnability of any game [8] by gradually increasing the search depth, , and checking if ⊧ (, ). For a game , we denote by the length of the longest valid playing sequence with player as the winner. Iterative deepening is complete and terminates as long as we are provided with : If ⊧ ̸ (, ) for all ≤ , then cannot strongly win the game at all. Computing is beyond the scope of this paper, and so we used human domain knowledge [21] to determine it.
Our overall approach is given in Figure 1.2 We use qasp2qbf [13] for the QASP to QBF translation. For the QBF preprocessing, we use bloqqer [24]. Finally, we solve the preprocessed formulas with one of the state-of-the-art QBF solvers Caqe [7]. Our approach is certainly not the only method of reasoning about the bounded-depth strong winnability of strategic games. Forward search algorithms are widely applied in solving such a problem. For comparison purposes, we implemented a naive Minimax Search-based solver (Minx) in C++ that uses Prolog as the GDL reasoner for legal actions [25] and an enhanced version with transposition tables (MinxTT). All the experiments were run on a Latitude 5430 laptop with a solving time limit of 900 seconds.
In Table 1, we record the value of and the smallest depth of the game in bold if the game can be proved to be strongly winnable by player within steps by any of the 3 solvers within the solving time limit. If player cannot force a win at all depths, and the game can be proved not to be strongly winnable by player within steps by any solver under any encoding in the solving time limit, we let = and record in plain format. For games that can neither be proved to be strongly winnable by at some depth nor be proved not to strongly winnable by for all depth within the solving time limit, we record the maximum refuted depth [21] (i.e., the maximum such that the game is proved not to be strongly winnable by within steps by any solver under any encoding within the solving time limit) of the unsolved games in italic format.
Caqe (Caqe+bloq) to verify (, ), the run time of the baseline minimax solver (Minx), and the run time of the minimax with transposition table solver (MinxTT).
(i.e., prove or disprove whether can strongly win the game) in a reasonable amount of time. For the relatively larger instances C-4-5x5 and C-4-6x6, although Caqe cannot solve the game completely, it can disprove the bounded-depth strong winnability property of these games to a relatively large depth. If we compare the QBF-based approach (Caqe+bloq) with the baseline minimax solver (Minx), we can observe that the eficiency of the QBF-based approach outperforms Minx in almost all instances except the easy ones, such as C-3, where the bloqqer preprocessing time dominates the solving procedure. The comparison between the QBF-based approach with the minimax and transposition table solver MinxTT, however, is mixed, and the result is highly domain dependent. Except for the easy domain such as C-3, the QBF-based approach outperforms MinxTT in most of the non-trivial games from C-4, GT-1-1, and
2The interested reader can find the code used in our experiments here: https://github.com/hharryyf/gdl2qbf-general
directly following Definition 4, and for verifying the bounded-depth strong winnability, the algorithm is similar to the baseline minimax search, which performs drastically worse than our QBF-based approach. Although with a transposition table, the eficiency of the minimax search solver for verifying the bounded-depth strong winnability can be improved significantly, for general GCL model-checking, it is still unclear how a transposition table can be properly defined. Our QBF-based approach is more generic because the learning mechanism within the QBF solver (e.g., Counterexample Guided Abstract Refinement [ 7]) applies to any QBF expression. Although the transposition table is not the same as the learning mechanism in QBF solvers, both can prune unnecessary search space. With a generic QBF solver, we can leverage its pruning efect without the need to design a transposition table from scratch.
In this paper, we investigate the connection between Coalition Logic and GDL and propose a QBF-based model-checking method. Although Coalition Logic is only a subset of ATL [4], it allows the formulation of both strategic and non-strategic properties up to a bounded depth. Our case study on solving two-player games shows that the QBF-based model-checking method has the potential to assist GGP systems in reasoning about endgame properties that can be formulated as GCL formulas. In the future, we plan to systematically evaluate our QBF-based approach on verifying other GCL properties and investigate how to integrate the QBF-based method into a GGP system. Also, we intend to investigate how to extend our approach to reason about GCL formulas of games with imperfect information [26].
During the preparation of this work, the authors used ChatGPT in order to: Grammar and spelling check.
[26] M. Thielscher, A general game description language for incomplete information games, in: Proceedings of AAAI, 2010, pp. 994–999.