Epistemic GDL: A Logic for Representing and Reasoning about Imperfect Information Games

1 Introduction

General Game Playing (GGP) is concerned with creating intelligent agents that understand the rules of arbitrary new games and learn to play these games without human intervention [Genesereth et al., 2005]. Representing and reasoning about games is a core technique in GGP. A formal game description language (GDL) has been introduced as an official language for GGP since 2005. GDL is defined as a high-level, machine-processable language for representing the rules of arbitrary games [Love et al., 2006]. Originally designed for perfect information games, GDL has recently been extended to GDL-II so as to incorporate imperfect information games, such as Poker, Backgammon [Thielscher, 2010].

Playing games with imperfect information poses an intricate reasoning challenge for players since imperfect information requires a player to use the rules of a game to infer legal actions, draw conclusions from her own knowledge about the current game state and about knowledge of other agents. However, as a purely descriptive language, GDL-II is only a tool for describing the rules of an imperfect information game but does not provide a facility for reasoning about how a player infers unveiled information based on the rules [Schiffel and Thielscher, 2011; 2014]. Indeed, some information is essential for players to proceed with a game.

For example, players should always know their own available actions in non-terminal states and know their results in terminal states. Such epistemic properties of a game are normally implied by the game rules and thus need reasoning facilities to infer and verify them. Unfortunately, GDL-II (or GDL) is not designed for this purpose. To handle this issue, a few approaches have been proposed, mostly embedding GDL-II into a logical system, such as Situation Calculus or Alternating-time Temporal Epistemic Logic (ATEL), to use their reasoning facilities [Schiffel and Thielscher, 2011; Ruan and Thielscher, 2011; 2012; Huang et al., 2013]. As long as the targeting logics are expressive enough to interpret any GDL description, it is possible to use the inference mechanisms of these logics for reasoning about GDL-II games. However, a highly expressive logic may incur high complexity for reasoning tasks. For instance, Ruan and Thielscher [2012] propose an adaption of ATEL to verify epistemic properties of GDL-II games, and show that the model-checking problem in that setting is 2EXPTIME-hard. Such high computational complexity may not be what we want.

This paper aims to propose a different approach to deal with this problem. We introduce a logical framework, called EGDL, equipped with a language for representing imperfect information games and a semantical model that can be used for reasoning about game information and players' epistemic status. More importantly, we develop a model-checking algorithm for EGDL and show that the complexity of the model-checking problem for the logic can be significantly reduced to ∆p2 . There are two major reasons that help us to reduce the complexity. Firstly, our language is a conservative extension of GDL with the standard epistemic operators [Fagin et al., 2003]. We take a cautious way of doing that without introducing the until operator or coalition operators. Secondly, we provide an imperfect recall semantics for knowledge. Other cases could be considered; nevertheless, the addition of perfect recall to GDL-II renders the model-checking problem of ATEL undecidable in general [Ruan and Thielscher, 2012]. Also, in many applications, especially when modeling extremely large games, imperfect recall may provide considerably empirical and practical advantages [Piccione and Rubinstein, 1997; Waugh et al., 2009; Busard et al., 2015]. Despite of a moderate expressive power, we demonstrate with a running example that our language is enough for expressing game rules, formalizing essential epistemic properties and specifying the interactions of knowledge and actions. In this sense, EGDL makes a good balance between expressive power and computational efficiency.

The rest of this paper is structured as follows: Section 2 establishes the syntax and the semantics of EGDL. Section 3 demonstrates its expressiveness and reasoning facility. Section 4 investigates the model-checking problem of EGDL. Finally, we conclude with a discussion of related work and future work.

2 The Framework

All games we consider in this paper are assumed to be played in multi-agent environments. A game signature S is a triple (N↪ A↪ Φ), where

• ÷ A = Si2N Ai , where Ai consists of a non-empty finite set of actions for agent i s.t. Ai \Aj = ; if i 6= j, and
• ÷ N = ¶1↪ 2↪ · · · ↪ k♦ is a non-empty finite set of agents,
• ÷ Φ = ¶p↪ q↪ · · · ♦ is a finite set of propositional atoms for specifying individual features of a game state.

Hereafter we will fix a game signature S and all concepts will be based on the same game signature unless otherwise specified.

2.1 Epistemic State TransitionModels

We begin by introducing the semantical structures used to model synchronous games with imperfect information. By synchronous we mean that all players move simultaneously. In particular, turn-based asynchronous games are modelled by only allowing the "noop" action for a player, when it is not her turn.

Definition 1. An epistemic state transition (ET) model M is a tuple (W↪ w↪ T↪ ¶Ri♦i2N ↪ L↪ U↪ g↪ V ), where

• ÷ w 2W, representing the initial state.
• ÷ W is a non-empty set of possible states.
• ÷ T ✓W, representing the set of terminal states.
• ÷ Ri ✓ W ⇥ W is an equivalence relation for agent i, indicating the states that are indistinguishable for i.
• ÷ L ✓ W ⇥A is a legality relation, describing the legal actions at each state.
• ÷ U : W ⇥D !W is an update function, specifying state transitions, where D is the set of joint actions Qi2N Ai .
• ÷ g : N ! 2W is a goal function, specifying the winning states for each agent.
• ÷ V : W ! 2Φ is a standard valuation function.

For d 2 D, let d(i) denote the i-th component of d. That is, agent i's action in the joint action d. For convenience, let L(w) = ¶a 2 A ♣ (w↪ a) 2 L♦ denote the set of all legal actions at state w. We now define the set of all possible ways in which a game can develop.

Definition 2. LetM = (W↪w↪ T↪ ¶Ri♦i2N↪ L↪U↪ g↪ V ) be an ET-model. A path δ is a sequence of states and joint actions w d1! · · · de! we such that for all 1  j  e and any i 2 N,

1. dj(i) 2 L(wj-1) (that is, any action that is taken must be legal),
2. wj = U(wj-1↪ dj) (state transition), and
3. ¶w↪ · · · ↪we-1♦\T = ; (that is, only the last state may be terminal).

A path δ is complete if we 2 T. Let P(M) denote the set of all complete paths in M. When M is fixed, we simply write P. Given δ 2 P, the states on δ are called reachable states. Let δ[j] denote the j-th reachable state of δ and ✓i(δ↪ j) denote the action of agent i taken at stage j of δ. The length of δ, written ♣δ♣, is defined as the number of actions.

The following definition, by extending equivalence relations over states to complete paths, characterizes precisely what an agent with imperfect recall and perfect reasoning can in principle know at a specific stage of a game.

Definition 3. Two complete paths δ, δ0 2 P are imperfect recall (also called memoryless) equivalent for agent i at stage j 2 N, written δ ⇡ji δ0 , iff δ[j]Riδ0 [j].

That is, imperfect recall requires an agent to be only aware of the present state but forget everything that happened. This is similar to the notion of imperfect recall in ATL [Schobbens, 2004]. It should be noted that the paper focuses on imperfect recall; nevertheless, the framework is flexible to define ATL state-based perfect recall [Jamroga and van der Hoek, 2004] and GDL-II perfect recall [Thielscher, 2010].

To illustrate our framework, we use as our running example a variant of the Tic-Tac-Toe, called Krieg-Tictactoe in [Schiffel and Thielscher, 2011].

Example. Krieg-Tictactoe is played by two players, cross x and naught o, who take turns marking grids in a 3⇥3 board. Different from standard Tic-Tac-Toe, each player can see her own marks, but not those of her opponent, just like the chess variant Kriegspiel [Pritchard, 1994]. Players are informed of the turn-taking. The game ends if the board is completely filled or one player wins by having completed a horizontal, vertical or diagonal line of three with her own symbol.

To represent Krieg-Tictactoe in terms of the ET-model, we first describe the game signature, written SKT , as follows: let NKT = ¶x↪ o♦, AiKT = ¶aij↪k ♣ 1  j↪ k  3♦ [ ¶noopi ♦, and ΦKT = ¶pij↪k ↪ tried(aij↪k )↪ turn(i) ♣ i 2 ¶x↪ o♦ and 1  j↪ k  3♦, where aij↪k denotes the action that player i fills grid (j↪ k) with her symbol, noopi denotes that player i does action noop, pij↪k represents the fact that grid (j↪ k) is filled with player i's symbol, tried(aij↪k ) represents the fact that player i has tried to fill grid (j↪ k) before, and turn(i) says that it is player i's turn now.

We next specify the ET-model for this game, written MKT , as follows: let WKT = ¶(tx↪ to↪ x1↪1↪ · · · ↪ x3↪3) : tx↪ to 2 ¶0↪ 1♦ & x1↪1↪ · · · ↪ x3↪3 2 ¶⇤↪⇥↪⇢↪⌦↪⊙♦♦ be the set of possible states, where tx, to specify the turn taking and xi↪j represents the fact that grid (i↪ j) is occupied by the cross and not tried by the nought ⇥, occupied by the nought and not tried by the cross ⇢, occupied by the nought and tried by the cross ⌦, occupied by the cross and tried by the nought ⊙, or empty ⇤. The initial state w is (1↪ 0↪⇤↪ · · · ↪⇤).

For any two states w = (tx↪ to↪ x1↪1↪ · · · ↪ x3↪3) and w0 = (t0x ↪ t0o ↪ x01↪1 ↪ · · · ↪ x03↪3 ) in WKT , wRxw0 iff (1) ti = t0i for any i 2 NKT , (2) xj↪k 2 ¶⇥↪⊙♦ iff x0j↪k 2 ¶⇥↪⊙♦ for any 1  j↪ k  3, and (3) xj↪k = ⌦ iff x0j↪k = ⌦ for any 1  j↪ k  3. The equivalence relation for o is defined in a similar way. Let VKT be a valuation such that for each state w = (tx↪ to↪ x1↪1↪ · · · ↪ x3↪3) 2 WKT , VKT(w) = ¶turn(i) : ti = 1♦ [ ¶pxj↪k : xj↪k 2 ¶⇥↪⊙♦♦ [ ¶poj↪k : xj↪k 2 ¶⇢↪ ⌦♦♦ [ ¶tried(axj↪k ) : xj↪k = ⌦♦ [ ¶tried(aoj↪k ) : xj↪k = ⊙♦. Moreover, we assume that each player takes the same action at stages of all her indistinguishable complete paths, i.e., ✓i(δ↪ j) = ✓i(δ0 ↪ j) whenever δ ⇡ji δ0 . Due to the space limit, we refrain from explicitly listing the legality relation, the update function, and the terminal and goal states for the agents as this is possible but considerably lengthy. However, the syntactic descriptions of the game given in the following section detail them in a more compact way.

2.2 The Language

Let us now introduce an epistemic extension of a variant of GDL [Zhang and Thielscher, 2015b] to represent games with imperfect information, and further provide a semantics for the language based on the epistemic state transition model. We call this framework EGDL for short.

Definition 4. The language, denoted by L, consists of

• ÷ pre-defined propositions: initial, terminal, wins(·), legal(·) and does(·);
• ÷ the finite set Φ of propositional atoms;
• ÷ logical connectives ≻ and ^;
• ÷ epistemic operators: K and C.
• ÷ temporal operator ©;

A formula ' in L is defined by the following BNF:

'::= p ♣initial ♣terminal ♣ legal(ai ) ♣ wins(i) ♣ does(ai ) ♣

Other connectives _, !, $, >, ? are defined by ≻ and ^ in a standard way. Intuitively, initial and terminal specify the initial state and the terminal states of a game, respectively; does(ai ) asserts that agent i takes action a at the current state; legal(ai ) asserts that action a is available to agent i at the current state; and wins(i) asserts that agent i wins at the current state. The formula ©' means "' holds in the next state". All these components are inherited from GDL. The epistemic operators K and C are taken from the Modal Epistemic Logic [Fagin et al., 2003]. The formula Ki' is read as "agent i knows '", and C' as "' is common knowledge among all the agents in N".

We use the following abbreviations in the rest of the paper:

where bKi and bC are the dual operators of Ki and C, respectively. bKi' says "' is compatible with agent i's knowledge" and it is similar to bC'. E' says "every agent in N knows '".

Let us illustrate the intuition of the language with our running example.

Example (continued) The rules of Krieg-Tictactoe are specified by EGDL in Figure 1.

Figure 1: An EGDL description of Krieg-Tictactoe.

The initial state, each player's winning states, the terminal states and the turn-taking are given by rules 1-4.

The preconditions of each action are specified by Rule 5 and Rule 6. The player who has the turn can fill any grid s.t. (i) it is not filled by herself, and (ii) she has never tried to fill the grid before. The other player can only do action noop.

Rules 7 and 8 are the combination of the frame axioms and the effect axioms [Reiter, 1991]. Rule 7 states that a grid is marked with a player's symbol in the next state if the player takes the corresponding action at the current state, or the grid has been filled by herself, or the game ends. Similarly, Rule 8 says that an action is tried by a player in the next state if the action is ineffective while still taken by the player at the current state, or it has been tried before, or the game ends.

The others are the epistemic rules. Rule 9 states each player knows which action she is taking. Rule 10 and Rule 11 says both players know the initial state and the turn-taking, respectively. Rule 12 says that each player knows which grid is filled or not by her own symbol. Similarly, Rule 13 states that each player knows which grid is tried or not by herself.

Let ⌃KT be the set of rules 1-13. It should be noted that rules 11-13 together specify the epistemic relations for each player: two states are indistinguishable for a player if their configurations of the game board are the same in her view.

2.3 Semantics

The semantics of the language is based on the epistemic state transition model.

Definition 5. Let M be an ET-model. Given a complete path δ in M, a stage j of δ and a formula ' 2 L, we say ' is true at j of δ under M, denoted by M↪ δ↪ j ♣= ', according to the following definition:

M↪ δ↪ j ♣= p iff p 2 V (δ[j]) M↪ δ↪ j ♣= ≻' iff M↪ δ↪ j 6♣= ' M↪ δ↪ j ♣= '1 ^'2 iff M↪ δ↪ j ♣= '1 andM↪ δ↪ j ♣= '2 M↪ δ↪ j ♣= initial iff δ[j] = w M↪ δ↪ j ♣= terminal iff δ[j] 2 T M↪ δ↪ j ♣= wins(i) iff δ[j] 2 g(i) M↪ δ↪ j ♣= legal(ai ) iff ai 2 L(δ[j]) M↪ δ↪ j ♣= does(ai ) iff ✓i(δ↪ j) = ai M↪ δ↪ j ♣=©' iff if j < ♣δ♣, then M↪ δ↪ j + 1 ♣= ' M↪ δ↪ j ♣= Ki' iff for any δ0 2 P with δ ⇡ji δ0 , M↪ δ0 ↪ j ♣= ' M↪ δ↪ j ♣= C' iff for any δ0 2 P with δ ⇡jN δ0 , M↪ δ0 ↪ j ♣= '

A formula ' is globally true in an ET-model M, written M ♣= ', if M↪ δ↪ j ♣= ' for any δ 2 P and any 0  j  ♣δ♣. A formula ' is valid, written ♣= ', if M ♣= ' for any ETmodel M. A formula ' is called true at a state w in M, written M↪w ♣= ', if it is true for all complete paths going through w, i.e., M↪ δ↪ j ♣= ' for any δ 2 P and any j ≥ 0 with δ[j] = w. Finally, let ⌃ be a set of formulas in L, then M is a model of ⌃ if M ♣= ' for all ' 2 ⌃.

where ⇡jN is its transitive closure of Si2N ⇡ji .

We now show that EGDL provides a sound description for Krieg-Tictactoe.

Proposition 1. MKT is a model of ⌃KT .

It follows that these game rules are common knowledge among two players, which is just what we expect.

3 Epistemic and Strategic Reasoning

In this section, we demonstrate the expressive power and flexibility of EGDL by showing how it allows us to specify epistemic properties and reason about agents' knowledge.

3.1 Epistemic Properties

The introduction of imperfect information raises new epistemic properties of a game. For instance, to make a game playable, each player should always know her own legal actions in the course of the game. This property as well as some other well-known properties can be naturally formulated by EGDL as follows: given i 2 N and ai 2 Ai ,

(1) initial ! C initial (2) legal(ai ) ! Ki(legal(ai )) (3) does(ai ) !Ki(does(ai )) (4) wins(i) !Ki(wins(i)) (5) terminal ! C terminal

Formulas (1) and (5) express that the initial state, the terminal states are common knowledge, respectively. Formula (2) says that each agent knows her own legal actions. In ATEL, this is a required semantic property yet with no syntactic expression [ ˚Agotnes, 2006]. Formula (3) asserts that each agent is aware of her own actions. This is called the "uniform" property of actions (strategies) also with no syntactic counterpart in ATEL [Van der Hoek and Wooldridge, 2003; Jamroga and van der Hoek, 2004]. Finally, formula (4) specifies that each agent should know her winning result.

Moreover, the above epistemic properties are precisely characterised by indistinguishable complete paths as follows:

Proposition 2. Let M be an ET-model. Then

1. M ♣= initial ! Cinitial iff for all δ↪ δ0 2 P and any j 2 N, if δ ⇡jN δ0 , then (δ[j] = w iff δ0 [j] = w).
2. M ♣= legal(ai ) ! Ki(legal(ai )) iff for all δ↪ δ0 2 P and any j 2 N, if δ ⇡ji δ0 , then (ai 2 L(δ[j]) iff ai 2 L(δ0 [j])).
3. M ♣= does(ai ) ! Ki(does(ai )) iff for all δ↪ δ0 2 P and any j 2 N, if δ ⇡ji δ0 , then (✓i(δ↪ j) = ai iff ✓i(δ0 ↪ j) = ai ).
4. M ♣= wins(i) !Ki(wins(i)) iff for all δ↪ δ0 2 P and any j 2 N, if δ ⇡ji δ0 , then (δ[j] 2 g(i) iff δ0 [j] 2 g(i)).
5. M ♣= terminal ! Cterminal iff for all δ↪ δ0 2 P and any j 2 N, if δ ⇡jN δ0 , then (δ[j] 2 T iff δ0 [j] 2 T).

Obviously, not all games with imperfect information satisfy these epistemic properties. For instance, property (5) does not hold for Krieg-Tictactoe. Consider the two reachable states depicted in Figure 2. They are indistinguishable

for player o. Yet the left one is a terminal state while the right one is not. In fact, according to the game rules, KriegTictactoe satisfies all the other properties.

Observation 1. Formulas (1)-(4) are globally true in MKT .

It should be noted that each EGDL-formula may be interpreted as a property of a game. Typically, globally true formulas describe properties for a particular game, such as the rules for Krieg-Tictactoe, while valid formulas specify general properties of a class of games and thus can be used to classify games. For instance, different fromKrieg-style board games, most card games have the property (5).

3.2 Strategic Reasoning

Let us now show how to use EGDL to reason about agents' knowledge and actions based on the game rules. In the context of imperfect information, epistemic reasoning is closely related to strategic reasoning. To start with, the following proposition shows that EGDL is suitable for reasoning about players' knowledge as it is a conservative extension of the standard Epistemic Modal Logic S5Cn [Fagin et al., 2003].

Proposition 3. Given an EGDL-formula ' without involving the operator © and the pre-defined propositions, ' is valid in EGDL iff it is valid in S5Cn .

This result indicates that EGDL is sufficient to provide a static characterization of agents' knowledge at a certain stage. For instance, with S5Cn , we can derive the following formulas from the rules of Krieg-Tictactoe.

Observation 2.

1. MKT ♣= turn(i) !Cturn(i)
2. MKT ♣= Ki(K-ip-i j↪k _ K-i≻p-i j↪k )
3. MKT ♣= Kitried(aij↪k) !Kip-i j↪k

Clause 1 says the turn-taking is common knowledge. Clause 2 says a player knows the opponent knows whether or not a grid is filled by herself. The last one says if a player knows she has tried an action, then she knows the corresponding grid has been filled by the opponent. The last two properties are important when players gather information.

Furthermore, with the full expressive power of the language, we can use EGDL to specify agents' knowledge of particular game features and reason about how agent's knowledge changes as a game progresses.

Observation 3.

1. MKT ♣= Kipij↪k !Ki©pij↪k
2. MKT ♣= Ki©tried(aij↪k) !©Kitried(aij↪k)
3. MKT ♣= does(aij↪k) !©Ki(pij↪k _ tried(aij↪k))
4. MKT ♣= initial ! C(V3j↪k=1 legal(axj↪k) ^ legal(noopo ))

Intuitively, clause 1 says that if a player knows a grid has been filled by herself, then she still knows this fact holds at the next state. Clause 2 says that a player is able to remember the grid she has tried to fill before. Clause 3 says that at the initial state the legal actions are common knowledge among two players, and Clause 4 expresses that if a player takes an action now, then at the next state she will know either the corresponding grid has been filled by her symbol or she has tried that action.

Most importantly, the interactions of actions and knowledge can be naturally formulated using EGDL. Specifically, they interact in three different ways:

(i) Knowledge is necessary for an agent to perform an action, which may be formulated by does(ai ) ! Ki'. For instance, in Krieg-Tictactoe, with partial observation, a player might take an ineffective action by trying to fill a grid which has been filled by the opponent. Then we say a player i takes a good action aij↪k , written good(aij↪k ), if it is effective. It follows that, to take a good action, a player needs to know the grid she attempts to fill is empty. Formally, MKT ♣= good(aij↪k ) !Ki(≻(pxj↪k _ poj↪k )).

(ii) Performing an action may increase an agent's knowledge, which may be specified by does(ai ) ! ©Ki'. For example, if a player takes an ineffective action, then she would know the corresponding grid has been filled by the other player. Consider the following complete path

(iii) An agent makes her choice of actions based on her knowledge, which may be captured by Ki' ! does(ai ). Let us consider the following two basic actions:

At stage 2 after player o tries to fill grid (2,2), by Rule 7 and Rule 13, she knows that the grid has been filled by player x. Thus, MKT ↪ δ↪ 1 ♣= does(ao2↪2 ) ! ©Ko(tried(ao2↪2 ) ^ px2↪2 ).

Intuitively, attack says if a player knows that filling a grid leads to win, then she should fill that grid. Instead, block says if a player knows her opponent makes to win by filling a grid in the next state, then the player must fill that grid at the current state to avoid an immediate loss.

4 Model Checking

In this section, we investigate the complexity of the modelchecking problem for EGDL and develop a model-checking algorithm for EGDL.

The model checking problem for EGDL, denoted by EGDL-MC, is the following: Given an EGDL-formula ', an ET-model M, a path δ of M and a stage j on δ, determine whether M↪ δ↪ j ♣= ' or not. In principle, two variants of EGDL-MC can be defined as follows: Given an ET-model M, a state w of M and an EGDL-formula ', determine whether M↪w ♣= ' and determine whether M ♣= '. It should be noted that all the bounds presented in this section remain true for these variants. Proofs are similar to those of EGDL-MC, or can be obtained by simple reductions to/from EGDL-MC.

Let us first consider the upper bound of the complexity for model-checking. Our goal is to show the following bound.

To prove this upper bound, according to the definition of ∆p2 , we need to prove that there is a polynomial-time deterministic Turing machine M with an NP-oracle such that M solves the model-checking problem for EGDL. To show the existence, let us start with a simple property of EGDL.

Let ' be an EGDL-formula, and M = (G↪ V ) be an ETmodel over S. Take to be any subformula of ' of the form ⊕#, where ⊕ is either C or Ki for some i 2 N. We introduce a fresh propositional atomp for . LetM be the ET-model (G↪ V ) where V is a valuation function defined by

for each state w of M. Let ' denote the formula obtained from ' by replacing by p . Then, by the definition of semantics for EGDL, the following property is clearly true.

Lemma 1. For every path δ of M and every stage j on δ, it holds that M↪ δ↪ j ♣= ' iff M ↪ δ↪ j ♣= ' .

Thus, by applying the above lemma, the epistemic operators can be eliminated from the formula in a recursive way. For the EGDL-formulas without epistemic operators, we can show that its model-checking problem is tractable.

Lemma 2. The following problem is in PTIME: Given an ET-model M, a path δ of M, a stage j on δ and an EGDLformula ' without involving any epistemic operators, determine whether M↪ δ↪ j ♣= ' or not.

Due to the space limit, we omit the proof here. Roughly speaking, in the context of model checking, the operator © can be simply regarded as a standard modal operator. Note that model-checking for the basic modal logic is in PTIME.

To construct the model M , the truth value of under M and a given state is needed to be evaluated. To simplify the question, let us first consider a simple case as follows.

Lemma 3. The following problem is in NP: Given an ETmodel M, a state w of M and an EGDL-formula ⊕' where ⊕ 2¶bC♦ [ ¶bKi : i 2 N♦ and ' does not involve any epistemic operators, determine whether M↪ w ♣= ⊕' or not.

This lemma holds due to the observation that, given any path δ of M and any j ≥ 0, we have M↪ δ↪ j ♣= ' if, and only if, M↪ δ[j↪ j + k]↪ 0 ♣= ', where k is the number of occurrences of © in ', and δ[j↪ j + k] denotes the segment of δ starting from position j with length k. With it, one can design a nondeterministic Turing machine which first guesses a path of length  k, and then check the truth value of ' under this path. By Lemma 2, the later can be done in PTIME.

To eliminate all the epistemic operators, it remains to consider the formulas with nested epistemic operator. With this complexity result for the non-nested case, we are now able to design an algorithm for the general case. Roughly speaking, the idea is to carry out the elimination of epistemic operator in a bottom-up way. As we can see in Algorithm 1, such an idea is implemented in the algorithm elimeop. It's easy to check

Input : an ET-model M and an EGDL-formula '

Output: an ordered pair (M0↪ '0)

begin

that the algorithm can be implemented in a polynomial-time deterministic Turing machine, but with an NP-oracle. Here the procedure of checking N0↪w ♣= b⊕≻ 0 is used as the NP-oracle. By Lemma 3, the checking is in NP. In addition, Algorithm elimeop visits each subformula of ' at most once, and that the number of subformulas of ' is not greater than the size of '. These assure that the Turing machine will terminate in a polynomial number of stages.

With this algorithm, we can then devise an algorithm mc for the model-checking of EGDL such that, given any proper M↪ δ↪ j and ' as input, mc works as follows:

• ÷ Firstly, mc call the algorithm elimeop(M↪ '), and let (M0↪ '0) be the results of this call.
• ÷ Next, mc check whether M0↪ δ↪ j ♣= '0 or not, and return "true" if it holds, "false" otherwise.

By Lemma 1 and the definition of algorithm elimeop, it is not difficult to verify that M↪ δ↪ j ♣= ' if, and only if, M0↪ δ↪ j ♣= '0. This assures the soundness of the algorithm mc. On the other hand, by the previous analysis, the first stage can be implemented in a polynomial-time determinitic Turing machine with an NP-oracle; by Lemma 2, the second stage can be done in PTIME. Thus, the algorithmmc can be implemented in a polynomial-time determinitic Turing machine with an NP-oracle, which proves Theorem 1.

Next we identify a lower bound of the complexity of model-checking for EGDL.

Theorem 2. EGDL-MC is ⇥p2 -hard.

Due to the space limit, we skip the proof here. The basic idea is to reduce the validity problem for Carnap's modal logic C to the model-checking problem of EGDL. The former has been proved to be ⇥p2 -complete [Gottlob, 1995].

It should be noted that the lower bound shows that the algorithm mc is nearly optimal, since ∆p2 and ⇥p2 are very close together, which both lie in the second level of the polynomial hierarchy.

5 Conclusion

We have presented a logical framework for representing and reasoning about imperfect information games with imperfect recall players. The framework allows us to represent game rules, formalize epistemic properties, specify the interactions of knowledge and actions as well as reason about agents' knowledge during game playing. We have also investigated the model-checking problem for the logic. These results indicate that we have made a reasonable compromise between expressive power and computational efficiency.

Most of the related work has been discussed in the Introduction. Besides that, the following is also worth mentioning. Ruan and Thielscher [2011] study the epistemic structure and expressiveness of GDL-II in terms of epistemic modal logic. They mainly provide a static characterization of players' knowledge at a certain stage without involving the temporal dimension. Haufe and Thielscher [2012] develop an automated reasoning method to deal with epistemic properties for GDL-II. Different from ours, their method is restricted to positive-epistemic formulas. Our underlying language is from [Zhang and Thielscher, 2015b]. It was originally proposed for reasoning about strategies of asynchronous games with perfect information, while we investigate its epistemic extension for representing and reasoning about synchronous games with imperfect information.

Directions of future research are manifold. As we have mentioned, besides imperfect recall, the framework is flexible enough to specify other memory types. To obtain a complete picture of the relation between perfect or imperfect information, and perfect or imperfect recall, we plan to study properties of these memory types; We also want to investigate the satisfiability problem and the axiomatization of EGDL based on the current literature [Zhang and Thielscher, 2015a; Halpern et al., 2004].

Acknowledgments

We are grateful to Michael Thielscher for his valuable suggestions, and special thanks are due to four anonymous referees for their insightful comments. This research was partially supported by ANR-11-LABX-0040-CIMI within the program ANR-11-IDEX-0002-02.