Guifei Jiang

Dongmo Zhang

Laurent Perrussel

Judgment Aggregation with Abstentions under Voters' Hierarchy

Similar to Arrow's impossibility theorem for preference aggregation, judgment aggregation has also an intrinsic impossibility for generating consistent group judgment from individual judgments. Removing some of the pre-assumed conditions would mitigate the problem but may still lead to too restrictive solutions. It was proved that if completeness is removed but other plausible conditions are kept, the only possible aggregation functions are oligarchic, which means that the group judgment is purely determined by a certain subset of participating judges. Instead of further challenging the other conditions, this paper investigates how the judgment from each individual judge affects the group judgment in an oligarchic environment. We explore a set of intuitively demanded conditions under abstentions and design a feasible judgment aggregation rule based on the agents' hierarchy. We show this proposed aggregation rule satisfies the desirable conditions. More importantly, this rule is oligarchic with respect to a subset of agenda instead of the whole agenda due to its literal-based characteristics.

Introduction

Judgment aggregation is an interdisciplinary research topic in economics, philosophy, political science, law and recently in computer science [START_REF] Dietrich | Arrow's theorem in judgment aggregation[END_REF][START_REF] Mongin | Consistent bayesian aggregation[END_REF][START_REF] Pigozzi | Belief merging and the discursive dilemma: an argument-based account to paradoxes of judgment aggregation[END_REF][START_REF] Wilson | On the theory of aggregation[END_REF][START_REF] Konieczny | Merging information under constraints: a logical framework[END_REF]. It deals with the problem of how a group judgment on certain issues, represented in logical propositions, can be formed based on individuals' judgments on the same issues. Although most of voting rules for social choice, such as majority, two-thirds majority or unanimity, are applicable to judgment aggregation, their behaviour can be significantly different due to possible logical links among the propositions on which a collective decision has to be made. A well-known example is the so-called doctrinal paradox [START_REF] Kornhauser | Unpacking the court[END_REF], which shows that the majority rule fails to guarantee consistent group judgments.

Suppose a court consisting of three judges has to reach a verdict in a breachof-contract case. There are three propositions on which the court is required to make judgments: p: The defendant was contractually obliged not to do a particular action. q: The defendant did that action. r: The defendant is liable for breach of contract.

According to legal doctrine, propositions p and q are jointly necessary and sufficient for proposition r, that is p ∧ q ↔ r. Now the three judges' judgments on the propositions are showed in Table 1.

Table 1. A doctrinal paradox p q r Judge 1 T T T Judge 2 T F F Judge 3 F T F Maj T T F If the three judges take a majority vote on proposition r which is regarded as the conclusion, the outcome is its rejection: a 'not liable' verdict. But if they take majority votes on each of p and q instead, then p and q are accepted and hence by the legal doctrine, r should be accepted as well: a 'liable' verdict. This specifically displays that the set of propositions {p, q, ¬r} which is accepted by a majority is logically inconsistent relative to the constraint p∧q ↔ r. The problem generalizes well beyond this example and does not depend on the presence of any legal doctrine or exogenous constraints [START_REF] List | The theory of judgment aggregation: an introductory review[END_REF].

To illustrate a more general problem, consider any set of propositions with logical connections. Suppose a three-member committee has to make group judgments (acceptance/rejection) on three logically interconnected propositions: p: We can afford a budget deficit. p → q: If we can afford a budget deficit, then we should spend more money on education. q: We should spend more money on education.

The individual judgments on given propositions for each member are shown in Table 2.

Table 2. A discursive dilemma p p → q q 1 T T T 2 T F F 3 F T F Maj T T F Then each individual holds consistent judgments on the three propositions, and yet there are majorities for p, p → q and ¬q, a logically inconsistent set of propositions. The first is the demand that in aggregating judgment a group should be responsive to the views of members on each of judgments involved. The second is the demand that in aggregating judgment a group should reach a collective set of judgments that is itself rational. The paradox shows that the two demands are sometimes in conflict, so that a group that tries to aggregate judgment faces a dilemma. The fact that majority voting may generate inconsistent group judgments is called the discursive dilemma [START_REF] Pigozzi | Belief merging and the discursive dilemma: an argument-based account to paradoxes of judgment aggregation[END_REF][START_REF] Pettit | Deliberative democracy and the discursive dilemma[END_REF][START_REF] Pivato | The discursive dilemma and probabilistic judgement aggregation[END_REF].

Naturally, the observation that majority voting may fail to produce consistent group judgments raises several questions. In particular, there are two fundamental questions: First, how general is the problem? Is it restricted to majority voting, or does it extend to other decision methods? Secondly, does it occur only in special situations, such as the breach-of-contract case, or does it arise more generally?

In response to these questions, a growing literature on the impossibility of consistent judgment aggregation under various conditions springs up. List and Pettit showed an impossibility result, similar to Arrow's impossibility theorem [START_REF] Arrow | A difficulty in the concept of social welfare[END_REF], that no aggregation rule can generate consistent group judgments if we require the rule to satisfy a set of "plausible" conditions [START_REF] List | Aggregating sets of judgments: An impossibility result[END_REF]. However, such an impossibility result did not discourage the investigation of the possibility of judgment aggregation. None of the conditions on either aggregation rules or decision problems, is indefectible. By weakening or varying these conditions, a growing body of literature on judgment aggregation has emerged in recent years [START_REF] Dietrich | Judgment aggregation (im)possibility theorems[END_REF][START_REF] List | Aggregating sets of judgments: Two impossibility results compared[END_REF][START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF][START_REF] Pauly | Logical constraints on judgement aggregation[END_REF][START_REF] Van Hees | The limits of epistemic democracy[END_REF].

Among all the plausible conditions that lead to impossibility results on judgment aggregation, completeness as one of the rationality requirements has received criticism of being overly demanding in many real-world situations, where an individual may abstain on a decision issue, and the group judgment on some issue may be undetermined. In fact, if we give up completeness, we are able to circumvent impossibility [START_REF] List | Aggregating sets of judgments: An impossibility result[END_REF][START_REF] Dietrich | Judgment aggregation with consistency alone[END_REF][START_REF] Dietrich | Judgment aggregation without full rationality[END_REF][START_REF] Dokow | Aggregation of binary evaluations with abstentions[END_REF][START_REF] Gärdenfors | A representation theorem for voting with logical consequences[END_REF]. Among them, Gärdenfors has proved a representation theorem for judgment aggregation without completeness, which shows that under certain fairly natural conditions, the only possible aggregation rules are oligarchic. Dietrich and List (2008) have strengthened Gärdenfors' results and showed that by giving up completeness in favor of deductive closure, oligarchies instead of dictatorships are obtained. However, this by no means is a negative result. In fact, our previous work [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] demonstrates that with abstentions, oligarchic aggregation is no longer a single level determination but can also be a multiple-level democracy, which partially explains its pervasiveness in the real world.

Since in our society the hierarchy is one of the most basic organization forms and a hierarchical group may give individual members or subgroups the priority to determine the group judgments on certain propositions. However, such kind of expert rights has been rarely investigated in the current literature [START_REF] Dietrich | A liberal paradox for judgment aggregation[END_REF], let alone proposing a specific judgment aggregation rule to formally display how the hierarchical groups generate the group judgments. In [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] we deal with this issue by proposing a quasi-lexicographic judgment aggregation rule which works well over the limited agenda. It mainly focuses on the following two questions: How does the hierarchical group generate the group judgments? How can the non-oligarchs have the power to make the collective decision in an oligarchic environment?

In this paper, we continue this line of research and investigate the question of whether we can generate consistent group judgments when giving different agents different weights depending on their hierarchy on the propositions in question. We focus on judgment aggregation with abstentions under voter's hierarchy. Our contributions can be summarized in the following: First, we amend the"plausible" conditions in [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF], which allows us to extend the set of propositions on which the quasi-lexicographic rule works well from a set of literals to logically interconnected formulas; Secondly, we propose a feasible literal-based aggregation rule for judgment aggregation with abstentions under voter's hierarchy, and show that it is neither dictatorial nor oligarchic over the whole set of agenda; Last but not least, to some extent, we circumvent the impossibility result in [START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF] by removing completeness from the requirements of both individual and collective levels.

The rest of this paper is structured as follows: In Section 2, we introduce the formal model of judgment aggregation with abstentions based on the formalisms in [START_REF] List | Aggregating sets of judgments: An impossibility result[END_REF][START_REF] Dietrich | A generalised model of judgment aggregation[END_REF]. In section 3, we list the conditions that sound natural in the context of abstentions and compare them with their counterparts in [START_REF] Dokow | Aggregation of binary evaluations with abstentions[END_REF][START_REF] Gärdenfors | A representation theorem for voting with logical consequences[END_REF][START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF]. In Section 4, we propose a literal-based lexicographic judgment aggregation procedure and investigate its properties. In the last section, we conclude the paper with a discussion of further work.

The Model of Judgment Aggregation with Abstentions

We consider a finite set of individuals N = {1, 2, . . . , n} with |N | ≥ 2. They are faced with a decision problem that requires group judgments on logically interconnected propositions represented by a logical language L with a set Φ 0 of atomic propositions and logical connectives {¬, ∨, ∧, ←, ↔}. We assume that the underlying logic of the logical language is the classical propositional logic with standard syntax and semantics. The set of literals which are either propositional variables or negations of propositional variables, is denoted by P, i.e., P = {p, ¬p | p ∈ Φ 0 }.

Given a decision-making problem, the set of propositions on which judgments are to be made is called the agenda. Formally, the agenda is a finite non-empty subset X ⊆ L that is closed under negation, i.e., if ϕ ∈ X, then ¬ϕ ∈ X, and under propositional variables, i.e., for all ϕ ∈ L, if ϕ ∈ X, then for all p ∈ Φ 0 occur in ϕ, p ∈ X. Let X 0 = X ∩ P be the set of literals included in the agenda. Consider the doctrinal paradox in Introduction as an example. In that situation, the agenda X is {p, q, p ∧ q, ¬p, ¬q, ¬(p ∧ q)}, and the set X 0 of literals in the agenda is {p, q, ¬p, ¬q}. Similar to [START_REF] Dietrich | Judgment aggregation without full rationality[END_REF], we assume that double negations in the agenda cancel each other. That is X = {ϕ, ¬ϕ : ϕ ∈ X * } where X * ⊆ L is a set of unnegated propositions.

We represent each individual judgment set as a subset of the agenda, which represents all the propositions that this individual accepts. The individual i's judgment set is denoted by Φ i , which is a subset of X. As we have mentioned in the previous section, we will not assume that each individual's judgment set must be complete. For each proposition ϕ ∈ X, it may happen that ϕ ∈ Φ i and ¬ϕ ∈ Φ i . In this case, we say that individual i abstains from making a judgment on ϕ, denoted by ϕ#Φ i . In other words, ϕ#Φ i if and only if ϕ ∈ Φ i and ¬ϕ ∈ Φ i . We assume that each individual's judgment satisfies the following conditions:

(Individual Logical Closure). For every ϕ ∈ X, if Φ i |= ϕ, then ϕ ∈ Φ i . (Individual Consistency). For every ϕ ∈ X, if ϕ ∈ Φ i , then ¬ϕ / ∈ Φ i .
The first condition requires that each individual judgment set is logically closed, that is for any ϕ in the agenda, if it is a logical consequence of an individual judgment set, then the individual accepts ϕ. The second condition specifies that each individual judgment set must be logical consistence, i.e., an individual cannot accept both ϕ and ¬ϕ for every proposition ϕ in the agenda. Given each individual's judgment set Φ i , the vector (Φ i ) i∈N is called a profile. For instance, the individual judgment set of each judge in the doctrinal paradox is as follows:

Φ 1 = {p, q, p ∧ q}; Φ 2 = {p, ¬q, ¬(p ∧ q)}; Φ 3 = {¬p, q, ¬(p ∧ q)}. They compose a profile.
Finally, an (judgment) aggregation rule is a function F that assigns to each admissible profile (Φ i ) i∈N a single group judgment set Φ ⊆ X, where ϕ ∈ Φ means that the group accepts ϕ. The set of admissible profiles is called the domain of F , denoted as Dom(F ). Note that we do not require the group judgments to be complete, which means that a group can also abstain from making a judgment on a proposition.

Conditions on Aggregation Rules

We now turn to investigating the conditions which are desirable to be put on an aggregation rule in terms of abstentions. Let F be an aggregation function. We first consider the following three conditions:

Universal Domain (UD). The domain of F includes all logically closed and consistent profiles (Φ i ) i∈N . Collective Rationality (CR). For all ϕ ∈ X and for all

(Φ i ) i∈N ∈ Dom(F ) F ((Φ i ) i∈N ) |= ϕ implies ϕ ∈ F ((Φ i ) i∈N ), and ϕ ∈ F ((Φ i ) i∈N ) implies ¬ϕ / ∈ F ((Φ i ) i∈N )
. This requires the collective judgment set is logical closed and consistent.

Non-dictatorship (ND).

There is no x ∈ N such that for all

{Φ i } i∈N ∈ Dom(F ), F ({Φ i } i∈N ) = Φ x .
This is a basic democratic requirement: no single individual should always determine the group judgment set.

The next condition is the counterpart of Unanimity with Abstentions in [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] which is restricted to literals.

Literal Unanimity with Abstentions (LU). For every α ∈ P, if there is some

V ⊆ N such that V = ∅, ∀i ∈ V.α ∈ Φ i and ∀j ∈ N \V .α#Φ j , then α ∈ F ((Φ i ) i∈N ).
Intuitively, if a set of individuals agrees on a certain judgment on a literal α while all the others abstain from α, then this condition requires that F ((Φ i ) i∈N ) should accept α as well.

As we will see in the following example, this new condition plays a crucial role in extending the agenda set from a set of literals to a set of logically interconnected formulas without generating inconsistent aggregate results. On the other hand, it is neither an extension nor a restriction of Unanimity without abstentions, also called Pareto optimality in [START_REF] Gärdenfors | A representation theorem for voting with logical consequences[END_REF] and Paretian condition in [START_REF] Dokow | Aggregation of binary evaluations with abstentions[END_REF], which is described as follows:

For every ϕ ∈ X, if ϕ ∈ Φ i for every i ∈ N , then ϕ ∈ F ((Φ i ) i∈N ).
The following proposition says that non-dictatorship can be derived from LU.

Proposition 1. Every judgment aggregation rule satisfying literal unanimity with abstentions is non-dictatorial.

Proof. Assume that F is dictatorial in some individual a ∈ N , then N/{a} = ∅. Take α ∈ X 0 and define α#Φ a and α ∈ Φ x for every x ∈ N/{a}. By literal unanimity with abstentions,

α ∈ F ((Φ i ) i∈N ), then F ((Φ i ) i∈N ) = Φ a , contradiction. ✷
The following independence condition requires that the group judgment on each literal should depend only on individual judgments on that literal, which is a counterpart of Arrow's "independence of irrelevant alternative" [START_REF] Arrow | Social Choice and Individual Values[END_REF]. With abstentions, this condition has two different versions:

Strong Literal Independence (LI s ). For every α ∈ P and every profiles

(Φ i ) i∈N , (Φ ′ i ) i∈N ∈ Dom(F ), if α ∈ Φ i ↔ α ∈ Φ ′ i for every i ∈ N , then α ∈ F ((Φ i ) i∈N ) ↔ α ∈ F ((Φ ′ i ) i∈N ).
Weak Literal Independence (LI). For every α ∈ P and every profiles

(Φ i ) i∈N , (Φ ′ i ) i∈N ∈ Dom(F ), if α ∈ Φ i ↔ α ∈ Φ ′ i and ¬α ∈ Φ i ↔ ¬α ∈ Φ ′ i for every i ∈ N , then α ∈ F ((Φ i ) i∈N ) ↔ α ∈ F ((Φ ′ i ) i∈N
). Note that these two versions are the same if we assume individual completeness. However, once we allow abstentions, these two versions become different and the strong version is intuitively too strong to be acceptable. Since in the profile even if all judges who abstain on α turn to rejecting α, no matter how big portion of these judges is, the strong version requires the group judgment on α to be the same so long as the same set of judges accepts α. The weak version solves the problem.

Similar conditions have been also discussed in the literature. It is not hard to see that the strong (weak) literal Independence condition strengthens the independence of irrelevant propositional alternatives condition in [START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF] to the set of literals under the provision of abstentions, while the weak independence condition amounts to reserving the independent of irrelevant alternatives condition in [START_REF] Dokow | Aggregation of binary evaluations with abstentions[END_REF] to literals.

The following two conditions are two versions of the counterpart of the neutrality condition, which requires that literals should be treated in an even-handed way by the aggregation function.

Strong Literal Neutrality (LN s ). For every α, β ∈ P and every profile

(Φ i ) i∈N ∈ Dom(F ), if α ∈ Φ i ↔ β ∈ Φ i for every i ∈ N , then α ∈ F ((Φ i ) i∈N ) ↔ β ∈ F ((Φ i ) i∈N ).

Weak Literal Neutrality (LN). For every α, β ∈ P and every profile (Φ

i ) i∈N ∈ Dom(F ), if α ∈ Φ i ↔ β ∈ Φ i and ¬α ∈ Φ i ↔ ¬β ∈ Φ i for every i ∈ N , then α ∈ F ((Φ i ) i∈N ) ↔ β ∈ F ((Φ i ) i∈N ).
Similarly, these two versions are the same if we assume individual completeness, and the strong version is intuitively too strong to be acceptable. Since in the profile even if all judges who abstain on α reject β, no matter how big portion of these judges is, the strong neutrality requires the group judgment on α and β to be the same so long as the set of judges accepting α and the set of judges accepting β are the same. The weak version solves the problem. The last condition is the counterpart of Systematicity, introduced by List and Pettit (2002), which combines independency and neutrality: literals should be treated in an even-handed way by the aggregation function; the group judgment on each literal should depend exclusively on the pattern of individual judgment on that literal.

Strong Literal Systematicity (LS s ). For every α, β ∈ P and every profiles

(Φ i ) i∈N , (Φ ′ i ) i∈N ∈ Dom(F ), if for every i ∈ N , α ∈ Φ i ↔ β ∈ Φ ′ i , then α ∈ F ((Φ i ) i∈N ) ↔ β ∈ F ((Φ ′ i ) i∈N ).
Weak Literal Systematicity (LS). For every α, β ∈ P and every profiles

(Φ i ) i∈N , (Φ ′ i ) i∈N ∈ Dom(F ), if for every i ∈ N , α ∈ Φ i ↔ β ∈ Φ ′ i and ¬α ∈ Φ i ↔ ¬β ∈ Φ ′ i , then α ∈ F ((Φ i ) i∈N ) ↔ β ∈ F ((Φ ′ i ) i∈N
). The reason why we reserve Independence, Neutrality and Systematicity to literals alone is based on the consideration that the problem of the doctrinal paradox and the discursive dilemma in Introduction comes from the requirement that the majority rule treats the compound formulas and propositional variables independently. Indeed the principle of compositionality, a fundamental presupposition of the semantics in most contemporary logics, denotes that the propositional variables are more primary than the compound formulas, since the truth of the later is determined by the truth of the former. For instance, in doctrinal paradox, the truth of the conjunctive formula p ∧ q is determined by its constituents p and q. In this sense, we may say the judgments on p and q are the reasons to accept p ∧ q or not, while the reason for whether p or q is accepted or not is beyond the expressivity of propositional logic. Of course in more powerful logic such as first-order logic, propositional variables are not primary atoms any more. In that more refined logic, once it presupposes the principle of compositionality, the new building blocks which replace propositional variables are the reasons for accepting propositional variables or not.

In the light of this thought, we take a reason-based perspective and apply the aggregation rule only to primary data whose reasons are beyond the expressivity power of the underlying logics, then use them to generate complex formulas within the underlying logic [START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF][START_REF] Nehring | Consistent judgement aggregation: the truth-functional case[END_REF]. Under abstentions, it is the literals instead of propositional variables that are primary data, since without completeness, we can not derive that p is rejected from that p is not accepted. It may be possible that p is abstained (neither accepted nor rejected). Therefore, we amount to reserving Independence, Neutrality and Systematicity to literals instead of propositional variables, which makes them more acceptable. For instance, one criticizes Systematicity (the independent part) being used for p ∨ q, where p denotes "The government can afford a budget deficit", and q "Forbidding smoking should be legalized" on the ground that there are two propositions involved, and that the society should know how each individual feels about either proposition, and not just about their disjunction. There is no similar objection arising when Systematicity applies to either p or q [START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF].

Another advantage is that this provides a plausible solution for the paradoxes in Introduction. For instance, we may just apply the majority rule to literals and calculate p, q in the group judgment set; then use them to generate p ∧ q in the group judgment set. According to this procedure, the group judgment set is {p, q, p ∧ q} which is logically consistent.

In the following we denote Universal Domain, Collective Rationality, Literal Unanimity with Abstentions and Weak Literal Systematicity as UD, CR, LU and LS for short.

The Literal-Based Lexicographic Aggregation Rule

In this section, we improve the work [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] by proposing an aggregation rule for judgment aggregation with abstentions under voters' hierarchy that works well over a set of logically interconnected formulas instead of a set of literals.

As we have mentioned in the introduction, we assume that there is a hierarchy among all the individuals. In the real-world we can easily see such a hierarchy, for instance, the management structure of an enterprise, a democratic political regime or a community organisation. Members in different ranks may play different roles in collective decision-making. Definition 1. A hierarchy over the set N of individuals is a strict partial order < over N that satisfies transitivity and asymmetry.

It follows that there is no infinite ascending sequence i 1 < i 2 < i 3 < • • • , where i n ∈ N , which means all hierarchical chains of N must be "up-bounded" with at least one top leader. In this sense, we say (N, <) is well-prioritized.

An aggregation rule determines which propositions are collectively accepted and which ones are collectively rejected. As we denoted, X 0 = X ∩ P is the set of literals included in the agenda. We first define an aggregate procedure F for that a literal α ∈ X 0 is collectively accepted, denoted by α ∈ F ((Φ i ) i∈N ), as follows:

Definition 2. For every α ∈ X 0 , α ∈ F ((Φ i ) i∈N ) iff ∀i ∈ N (¬α / ∈ Φ i ∨∃j ∈ N (i < j∧α ∈ Φ j )) and ∃k ∈ N.α ∈ Φ k (1)
Intuitively, this aggregate procedure says that a literal α is accepted by a group if the following two conditions are both satisfied.

(1) for any individual if he rejects α, then there is an individual with higher hierarchy accepting α; and (2) there is at least one individual accepting α.

We denote the set of collectively accepted literals by F ((Φ i ) i∈N ) 0 . Based on this concept, we define that any ϕ ∈ X is collectively accepted as follows:

Definition 3. For any ϕ ∈ X, ϕ ∈ F ((Φ i ) i∈N ) iff F ((Φ i ) i∈N ) 0 |= ϕ (2)
This definition says that a proposition ϕ in the agenda X is collectively accepted if it is a logical consequence of the set of collectively accepted literals. Similarly, a proposition ϕ ∈ X is collectively abstained if neither itself nor its negation is collectively accepted. That is,

ϕ#F ((Φ i ) i∈N ) iff ϕ / ∈ F ((Φ i ) i∈N ) and ¬ϕ / ∈ F ((Φ i ) i∈N ). (3)
We call above defined judgment aggregation rule F the literal-based lexicographic rule since we just apply the lexicographic rule to the subset of literals in the agenda.

To demonstrate how this rule works, let us consider the following example.

Example 1. Suppose Ann, Bill and Tom have to make group judgments on three logically connected propositions as follows:

p: There is the elixir of life. q: People can be immortal. p → q: If there is the elixir of life, then people can be immortal.

Ann thinks p is true and abstains on q and p → q, Bill rejects q and abstains on p and p → q, Tom accepts q and p → q, and abstains on p. Their individual judgments are shown as follows:

Table 3.

p q p→q Ann T # # Bill # F # Tom # T T
The hierarchy among them is Ann < Bill and Tom < Bill as illustrated below: Bill Ann Tom Note that individuals with the highest priority are written at the top of the diagram. We next apply the literal-based aggregation rule to generate the collective judgment set. The model of this aggregation situation is as follows:

-N = {Ann, Bill, T om} with Ann< Bill and Tom< Bill; -X = {p, q, p → q, ¬p, ¬q, ¬(p → q)} and X 0 = {p, q, ¬p, ¬q}.

The individual judgment sets for Ann, Bill and Tom are as follows:

• p ∈ Φ Ann , q#Φ Ann , p → q#Φ Ann ; • p#Φ Bill , ¬q ∈ Φ Bill , p → q#Φ Bill ; • p#Φ T om , q ∈ Φ T om , p → q ∈ Φ T om .
We first calculate the group judgments on the set X 0 of literals by Definition 2.

-The collective accepts p, since all of them don't reject p, i.e., ∀i ∈ N (¬p / ∈ Φ i ) holds, and Ann accepts p, i.e., ∃j ∈ N (p ∈ Φ j ) holds.

-The collective rejects q, since Bill with the highest priority rejects q, even though Tom accepts q.

Then the collective accepts p and rejects q, i.e., F ((Φ i ) i∈N ) 0 = {p, ¬q}. And by Definition 3, the collective rejects (p → q), since {p, ¬q} |= ¬(p → q). Thus, the group judgment set is {p, ¬q, ¬(p → q)} by the literal-based lexicographic aggregation rule.

We would like to remind that the quasi-lexicographic rule in [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] fails to deal with this situation, since the agenda involves logically interconnected formula p → q. If we apply that rule to this agenda, we could get an inconsistent aggregate result {p, ¬q, p → q}.

Moreover, the literal-based lexicographic aggregation rule provides a plausible solution to the paradox in Introduction. Let's consider the discursive dilemma. We may take all the possible hierarchy among the three agents into consideration. One boss case: let 1 < 2 < 3 be the hierarchy, then according to this rule the aggregate result is just the individual aggregate set of the first agent {p, q, p → q}, which is consistent. Yet the cost of this case is that the first agent seems to be the dictator for this profile, which is a bit depressing. Two-boss case: let the priority order be 1 < 3 and 1 < 2, then in the virtue of this rule, they collectively reject q and abstain on p and p → q. Three-boss (no boss or anonymity) case: according to this rule, p, q and p → q are all collectively abstained.

We next investigate the properties of the literal-based lexicographic rule F . The first proposition shows that the literal-based lexicographic rule F satisfies above desirable conditions UD, CR, LU and LS.

Theorem 1. The literal-based lexicographic rule F satisfies conditions UD, CR, LU and LS.

Proof. It is straightforward that F satisfies conditions UD according to the definition.

We next show F satisfies CR. (Logical Closure) For any ϕ ∈ X and for all {Φ i } i∈N , assume

F ({Φ i } i∈N ) |= ϕ. Since F ({Φ i } i∈N ) 0 |= F ({Φ i } i∈N ) (F ({Φ i } i∈N ) 0 |= ψ for any ψ ∈ F ({Φ i } i∈N )), so F ({Φ i } i∈N ) 0 |= ϕ, so ϕ ∈ F ({Φ i } i∈N ) by Definition 3.
(Consistence) We first show for any α ∈ P, α ∈ F ({Φ i } i∈N ) 0 implies ¬α ∈ F ({Φ i } i∈N ) 0 . Suppose for a contradiction that for some

β ∈ P, β ∈ F ({Φ i } i∈N ) 0 and ¬β ∈ F ({Φ i } i∈N ) 0 , then (i) ∀i ∈ N (¬β / ∈ Φ i ∨ ∃j ∈ N (i < j ∧ β ∈ Φ j )) and ∃k ∈ N.β ∈ Φ k ; (ii) ∀i ∈ N (β / ∈ Φ i ∨ ∃j ∈ N (i < j ∧ ¬β ∈ Φ j )) and ∃k ∈ N.¬β ∈ Φ k . By (i), (ii) we can get an infinite ascending sequence i 1 , i 2 , i 3 , • • • , which is a contradiction with that (N, <) is well-prioritized. Then F ({Φ i } i∈N ) 0 is consistent, so by the Definition 3, F ({Φ i } i∈N ) is consistent as well.
For LU, assume for every α ∈ P, if there is some

V ⊆ N such that V = ∅, ∀i ∈ V.α ∈ Φ i and ∀j ∈ N \V .α#Φ j , then by Definition 2, α ∈ F ({Φ i } i∈N ).
For LS, given every α ∈ P, the individuals accepting α and these rejecting α are the same for every two profiles (Φ i ) i∈N , (Φ ′ i ) i∈N , then the aggregate results of α according to the Definition 2 are the same as well. Yet it is not the case for LS s , for we could construct a counterexample: given a hierarchy on an agent set N = {1, 2, 3} with 1 < 2, 1 < 3. For the profile (Φ i ) i∈N where α ∈ Φ 1 , α#Φ 2 and α#Φ 3 , we have α ∈ F (Φ i ) i∈N by LU . Let individual 2, 3 who abstain on it turn to rejecting α, while individual 1 still accepts α, we get a different profile

(Φ ′ i ) i∈N , where α ∈ Φ ′ 1 , ¬α ∈ Φ ′ 2 and ¬α ∈ Φ ′ 3 , but α / ∈ F (Φ ′ i ) i∈N . ✷
As we expected, F satisfies the four desirable conditions and thus is a feasible aggregation rule for hierarchical groups to generate group judgments. One may be surprised to find that as an 'unfair' aggregation rule, F is non-dictatorial by Proposition 1. On the other hand, this shows that non-dictatorship is a very weak condition imposed on judgment aggregation functions when abstention is allowable. Gärdenfors and Dietrich et al have both showed that by giving up completeness, oligarchies instead of dictatorships are obtained [START_REF] Dietrich | Judgment aggregation without full rationality[END_REF][START_REF] Gärdenfors | A representation theorem for voting with logical consequences[END_REF]. We investigate whether this proposed rule is oligarchic. The definition of an oligarchic rule is given as follows: Definition 4. An aggregation rule G satisfying UD is a weak oligarchy if there is a non-empty smallest subset M ⊆ N such that for every profile

(Φ i ) i∈N ∈ Dom(G), i∈M Φ i ⊆ G((Φ i ) i∈N ).
And an oligarchic rule G is strict if for every profile

(Φ i ) i∈N ∈ Dom(G), i∈M Φ i = G((Φ i ) i∈N ).
In this case, we call G to be weakly (strictly) oligarchic with respect to M.

That is, an aggregation rule satisfying universal domain is said to be weakly oligarchic if there is a non-empty smallest set M such that for any profile of individual judgment set, the group judgment set contains all the propositions if they are in every member's judgment set of M . Furthermore, we say an aggregation rule is strictly oligarchic if for any profile of individual judgment set, the group judgment set is exactly the set of propositions that are in every member's judgment set of M . Special cases of weak oligarchic aggregation rules are unanimous (M = N ), majority (|M | > n 2 ) and dictatorial (M = {i}) rules. Specifically, the unanimous and dictatorial rules are weakly and strictly oligarchic rules, majority rule is weakly but not strictly oligarchic. However, the literal-based lexicographic rule F is neither weakly oligarchic nor strictly oligarchic. Here is a simple counter-example.

Let the agent set N = {1, 2} with <= ∅ , the agenda X = {p, q, p → q, ¬p, ¬q, ¬(p → q)} and the set of literals in the agenda X 0 = {p, q, ¬p, ¬q}, the individual judgment set for each agent is as follows: Φ 1 = {p, q, p → q}, Φ 2 = {¬p, ¬q, p → q}. Then Φ 1 ∩ Φ 2 = {p → q}, but according to the literalbased aggregation rule F , p#F (Φ 1 , Φ 2 ), q#F (Φ 1 , Φ 2 ) and p → q#F (Φ 1 , Φ 2 ). Thus,

Φ 1 ∩ Φ 2 ⊆ F (Φ 1 , Φ 2 ).
It may be a bit surprising to find that the literal-based aggregation rule is not oligarchic. In fact this does not violates the results in [START_REF] Dietrich | Judgment aggregation without full rationality[END_REF][START_REF] Gärdenfors | A representation theorem for voting with logical consequences[END_REF] since their conditions imposed on the aggregation rules are more strengthened than ours. Specifically, the unanimity and systemacity conditions hold for all formulas while we restrict them to literals. On the other hand, our proposed rule is literalbased, and the compound formulas are dependent on the collective judgments on the literals instead of generating by this rule. That is, if a formula is a logical consequence of the collective literals, then it is in the collective set; otherwise, it is abstained. Therefore, Instead of the whole agenda, we need to consider the oligarchy notion with respect to the set of literals in the agenda on which the literal-based aggregation rule takes effect. This idea leads to a weak concept of an oligarchic aggregation rule as follows: Definition 5. An aggregation rule G satisfying UD is a weak oligarchy w.r.t X 0 if there is a non-empty smallest subset M ⊆ N such that for every profile

(Φ i ) i∈N ∈ Dom(G), {ϕ ∈ X | i∈M Φ i ∩ X 0 |= ϕ} ⊆ G((Φ i ) i∈N ).
And an oligarchic rule G is strict w.r.t X 0 if for every profile

(Φ i ) i∈N ∈ Dom(G), {ϕ ∈ X | i∈M Φ i ∩ X 0 |= ϕ} = G((Φ i ) i∈N ).
Intuitively, an aggregation rule satisfying universal domain is said to be weakly oligarchic w.r.t X 0 if there is a non-empty smallest set M such that for any profile of individual judgment set, the group judgment set contains all the consequences of literals that are in every member's judgment set of M . Similarly, an aggregation rule is strictly oligarchic w.r.t X 0 if for any profile of individual judgment set, the group judgment set is exactly the set of consequences of the literals that are in every member's judgment set of M .

We have the following proposition saying the literal-based lexicographic rule F is weakly oligarchic w.r.t X 0 , but not strictly oligarchic w.r.t X 0 .

Proposition 2. The literal-based lexicographic rule F is weakly oligarchic w.r.t X 0 , but not strictly oligarchic w.r.t X 0 .

Proof. Suppose F satisfies universal domain, it suffices to find a non-empty smallest set M ⊆ N , such that for every profile of individual judgment sets

(Φ i ) i∈N , every ϕ ∈ X, if i∈M Φ i ∩ X 0 |= ϕ, then ϕ ∈ F ((Φ i ) i∈N ). Let O = M ax ≥ (N ) = {i ∈ N : ∄j ∈ N.i < j}. Since (N, <) is well-prioritized and |N | ≥ 2
, so O must exist and be non-empty. Suppose for every profile of individual judgment sets (Φ i ) i∈N , every i ∈ N and for all α ∈ X 0

, if α ∈ i∈O Φ i , then according to Definition 2, α ∈ F ((Φ i ) i∈N ). Then i∈O Φ i ∩ X 0 ⊆ F ((Φ i ) i∈N ) 0 . Since i∈O Φ i ∩X 0 |= ϕ, so F ((Φ i ) i∈N ) 0 |= ϕ, so ϕ ∈ F ((Φ i ) i∈N ) by Definition 3. We next show O is the smallest one with {ϕ ∈ X | i∈O Φ i ∩ X 0 |= ϕ} ⊆ F ((Φ i ) i∈N ). Suppose not, then there is some A ⊆ N such that A ⊂ O and {ϕ ∈ X | i∈A Φ i ∩ X 0 |= ϕ} ⊆ F ((Φ i ) i∈N ), then there is some a ∈ N such that a ∈ O but a / ∈ A. Take some β ∈ X 0 and define β ∈ Φ i for every i ∈ N \{a} and ¬β ∈ Φ a , then by Definition 2, β / ∈ F ((Φ i ) i∈N ), but β ∈ {ϕ ∈ X | i∈A Φ i ∩ X 0 |= ϕ}, contradicting with assumption. Thus, O is just the required M.
It's easy to construct a profile such that i∈M Φ i ∩ X 0 ⊇ F ((Φ i ) i∈N ) by LU. Take α ∈ X 0 and define α#Φ a for some a ∈ M and α ∈ Φ x for every x ∈ N/{a}. By literal unanimity with abstentions, α ∈ F ((Φ i ) i∈N ), but α ∈ i∈M Φ i ∩ X 0 . Thus F is not strictly oligarchic w.r.t X 0 . ✷ On the one hand the literal-based lexicographic aggregation rule F satisfies all the desirable conditions given in Section 3; on the other hand, it is only oligarchic with respect to the subset of literals in the agenda not over the whole set of agenda due to its literal-base characteristics.

The last proposition of this section shows under which conditions two literalbased lexicographic rules are identical. We first introduce a helpful notation. For any i ∈ N and any ϕ, ψ ∈ X, the individual i makes the same judgment on ϕ and ψ is denoted by

Φ i | {ϕ} ⇔ Φ i | {ψ} , that is Φ i | {ϕ} ⇔ Φ i | {ψ} is equivalent to (ϕ ∈ Φ i iff ψ ∈ Φ i ) and (¬ϕ ∈ Φ i iff ¬ψ ∈ Φ i ).
Proposition 3. Let {p} ⊆ X ∩ Φ 0 , and f 1 , f 2 be two literal-based lexicographic rules. If for all profiles of individual judgment sets

(Φ i ) i∈N , f 1 ((Φ i ) i∈N )| {p} ⇔f 2 ((Φ i ) i∈N )| {p} , then for all ϕ ∈ X, f 1 ((Φ i ) i∈N )| {ϕ} ⇔ f 2 ((Φ i ) i∈N )| {ϕ} .
Proof. Take any q ∈ X ∩ Φ 0 . Define the profile (Φ ′ i ) i∈N in terms of (Φ i ) i∈N as follows: for all i ∈ N , Φ ′ i = Φ i except at p where

Φ ′ i | {p} ⇔ Φ i | {q} . Then f 1 ((Φ i ) i∈N )| {q} ⇔ f 1 ((Φ i | {q} ) i∈N ) by LI ⇔ f 1 ((Φ ′ i | {p} ) i∈N ) by LS ⇔ f 1 ((Φ ′ i ) i∈N )| {p} by LI ⇔ f 2 ((Φ ′ i ) i∈N )| {p} by hypothesis ⇔ f 2 ((Φ ′ i | {p} ) i∈N ) by LI ⇔ f 2 ((Φ i | {q} ) i∈N ) by LS ⇔ f 2 ((Φ i ) i∈N )| {q} by LI. It is clear that f 1 ((Φ i ) i∈N ) ∩ Φ 0 = f 2 ((Φ i ) i∈N ) ∩ Φ 0 . Hence, f 1 ((Φ i ) i∈N ) = f 2 ((Φ i ) i∈N ). ✷
This proposition says that if two literal-based lexicographic rules make a same judgment (acceptance, rejection and abstention) on a propositional variable in the agenda, then they make the same judgment on all the formulas in the agenda.

In the other word, a literal-based lexicographic rule is determined by its responses to all the possible judgments (acceptance, rejection and abstention) on a fixed propositional variable in the agenda. This property paves the way to show a characterization result of the literal-based lexicographic rule. We leave this work for future.

Conclusion

In this paper, we have proposed a literal-based lexicographic rule which extends the set of agenda from a set of literals to a set of logically interconnected formulas [START_REF] Jiang | Judgment aggregation with abstentions: A hierarchical approach[END_REF] and further investigated the properties of this rule. It turns out that this proposed rule is neither dictatorial nor oligarchic in the standard sense. The reason for non-dictatorship is that, as proved in Proposition 1, we may take advantage of the abstention to show all individuals fail to play a role in collective decision-making on a particular proposition when they abstain from that proposition. This indicates that under the provision of abstentions, non-dictatorship is a rather weak condition imposed on the judgment aggregation rule. The reason for non-oligarchy is due to its literal-based characteristics. In fact, we may regard this proposed rule as a special case of premiss-based rule [START_REF] Dietrich | The premiss-based approach to judgment aggregation[END_REF] where the set of premisses is the subset of literals in the agenda.

There are many directions for future investigations. Firstly, as a special kind of lexicographic rule, it is interesting to investigate a representation result for our proposed aggregation rule. The lexicographic rule has been extensively studies in preference aggregation, and [START_REF] Andréka | Operators and laws for combining preference relations[END_REF] has proved that lexicographic rule is the only way of combining preference relations satisfying five natural conditions which are very close to Arrow's conditions. We expect to obtain a similar characterization result for our proposed rule. This work is under way;

Secondly, under the provision of abstentions, we have amended the commonly desirable conditions. It is natural to investigate some possibility results with respect to these amending conditions. In terms of the rationality requirements, this means that we drop the completeness condition. Comparing with the impossibility results, we get a possibility result which can be stated as: there are non-dictatorial aggregation rules satisfying universal domain, collective rationality, literal unanimity with abstentions and weak literal systematicity, which seems positive news to the result in [START_REF] Mongin | Factoring out the impossibility of logical aggregation[END_REF]. However, it is not the case since we do not assume completeness at both individual and collective levels, which means that a judge can abstain from a proposition and the group judgment on a proposition can be undetermined.

In addition, with abstentions, the dictatorship in judgment aggregation can also vary in degrees [START_REF] Rossi | Aggregating preferences cannot be fair[END_REF]. It is highly interesting to investigate the possibility scope between rationality, dictatorship under a set of plausible conditions. Some work has been done in this direction [START_REF] Dietrich | Propositionwise judgment aggregation: the general case[END_REF].

Last but not least, since the universal and perfect aggregation rule does not exist, a plausible way is to boil down aggregation problems to three-sided matching questions between specific so-called degenerate rules, specific groups and specific agendas., which is a promising direction [START_REF] Dietrich | A liberal paradox for judgment aggregation[END_REF].

Fig. 1 .

 1 Fig. 1.


Guifei Jiang

Dongmo Zhang

Laurent Perrussel

GDL Meets ATL: A Logic for Game Description and Strategic Reasoning

This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternatingtime Temporal Logic and prioritised strategy connectives. Our semantics is built upon the standard state transition model. The new framework allows us to formalise van Benthem's game-oriented principles in multiplayer games, and formally derive Weak Determinacy and Zermelo's Theorem for two-player games. We demonstrate with a real-world game how to use our language to specify a game and design a strategy, and how to use our framework to verify a winning/no-losing strategy. Finally, we show that the model-checking problem of our logic is in 2EXPTIME with respect to the size of game structure and the length of formula, which is no worse than the model-checking problem in ATL ⋆ .

Introduction

Logical analysis of games has been an important topic across the study of game theory, mathematics, philosophy and computer science [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Chatterjee | Strategy logic[END_REF][START_REF] Van Der Hoek | A logic for strategic reasoning[END_REF][START_REF] Kaneko | Game logic and its applications[END_REF][START_REF] Parikh | The logic of games and its applications[END_REF][START_REF] Pauly | Game logic-an overview[END_REF][START_REF] Van Benthem | Reasoning about strategies[END_REF]. It deals with the problems of [START_REF] Alur | Alternating-time temporal logic[END_REF]. how to specify a game situation, [START_REF] Chatterjee | Strategy logic[END_REF]. how to represent a game strategy and, more importantly, [START_REF] Van Der Hoek | A logic for strategic reasoning[END_REF]. how to model strategic reasoning of game players. A number of logical formalisms have been proposed to tackle these problems from different perspectives.

To deal with the first problem, Parikh and Pauly proposed a logical framework in which a game is treated as a program so that different games can be combined by program connectives [START_REF] Parikh | The logic of games and its applications[END_REF][START_REF] Pauly | A modal logic for coalitional power in games[END_REF]. Kaneko proposed another approach to game description by specifying each single game as a propositional logic theory [START_REF] Kaneko | Game logic and its applications[END_REF]. A more practical approach to specify a game by the so-called Game Description Language (GDL) [START_REF] Genesereth | General game playing: Overview of the AAAI competition[END_REF]. The language is much less expressive than the above mentioned game logics, but rich enough for describing any finite combinatorial games. This language has been used as an official language for General Game Playing since 2005.

To address the second problem, a number of approaches have been proposed for representing game strategies [START_REF] Chatterjee | Strategy logic[END_REF][START_REF] Van Benthem | Reasoning about strategies[END_REF][START_REF] Mogavero | Reasoning about strategies[END_REF][START_REF] Ramanujam | Dynamic logic on games with structured strategies[END_REF][START_REF] Zhang | Representing and reasoning about game strategies[END_REF]. The simplest way to represent a game strategy is to express a strategy as an action so that simple strategies can be combined into more complicated strategies using PDL connectives [START_REF] Van Benthem | Reasoning about strategies[END_REF][START_REF] Ramanujam | Dynamic logic on games with structured strategies[END_REF]. Zhang and Thielscher recently introduced another approach to represent game strategies [START_REF] Zhang | Representing and reasoning about game strategies[END_REF]. With their framework, a strategy is represented as a logical formula in GDL. More importantly, strategies can be combined by using a pair of prioritised logical connectives.

Some recent work has been done to tackle the third problem, mostly based on either Pauly's Coalition Logic (CL) or Alur et al's Alternating-time Temporal Logic (ATL) [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Pauly | A modal logic for coalitional power in games[END_REF]. Both logics use coalition modalities to specify strategic abilities of coalitions. However, these logics use existential quantifiers to express players' strategic abilities, such as 'a coalition of players has a strategy to achieve a game property', while description of strategies is not part of the logical language [START_REF] Van Benthem | In praise of strategies[END_REF]. There has been some work that extends ATL with explicit expression of game strategies by adding a strategy term into coalitional operators to mean a coalition commits to a strategy [START_REF] Van Der Hoek | A logic for strategic reasoning[END_REF][START_REF] Herzig | Reasoning about actions meets strategic logics[END_REF][START_REF] Walther | Alternating-time temporal logic with explicit strategies[END_REF]. However, strategies in their languages have to be in atomic forms with no internal structures.

None of the above mentioned work can deal with all three problems within a single logical framework. This is actually a serious problem because without explicitly specifying game rules, without expressing the strategies under consideration, we are unable to reason about the effects of these strategies. We need a comprehensive logical language and associated inference mechanism to define, compare and reason about strategies. In this paper, we propose a logical language by extending GDL with coalition operators and prioritised connectives [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Genesereth | General game playing: Overview of the AAAI competition[END_REF][START_REF] Zhang | Representing and reasoning about game strategies[END_REF]. Inherited from GDL, the proposed logical language can describe any finite perfect information game. Furthermore, by using Zhang and Thielscher's prioritised connectives and ATL-like coalition operators, the language can represent complicated game strategies and specify strategic abilities of players. More importantly, we provide unified semantics for both GDL-and ATL-formulas, which allows us to formalize the game-playing principles introduced by van Benthem [START_REF] Van Benthem | Reasoning about strategies[END_REF]. These principles make it possible to formally derive two well-known results for twoplayer games: Weak Determinacy and Zermelo's Theorem. Meanwhile, we use a generalised Gomuko game to demonstrate how to use our logical formalism to describe a game strategy and reason about strategies. Finally, we present an upper bound of the model-checking complexity of our logic.

The rest of this paper is structured as follows. Section 2 establishes the syntax and semantics of our proposed logical framework. Section 3 deals with the syntactical representation of strategies and demonstrates how to design strategies and reason about strategies in our framework. Section 4 discusses the modelchecking problem of the logic. Finally we conclude the paper with a discussion of future work.

The Logical Framework

In this section, we will introduce a logical language for specifying game rules and representing game strategies, and provide semantics of the language based on the state transition model. We call the framework the logic for Game Description and strategic Reasoning, denoted by GDR for short.

The Syntax

The language, denoted by L, consists of the following components. Let N be a finite set of agents and Φ a countable set of propositional atoms. For each a ∈ N , A a is a finite set of actions that agent a can perform. We assume that A a ∩ A b = ∅ if a = b and let A = a∈N A a . A formula ϕ in L is defined by the following BNF:

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | initial | terminal | does(α) | wins(a) | turn(a) | ϕ | ϕ▽ϕ | [C]ϕ | [[C]]ϕ where p ∈ Φ, a ∈ N , α ∈ A and C ⊆ N .
Besides the standard propositional connectives1 , initial and terminal are two logical constants, specifying the initial state and the terminal states of a game. does(.), wins(.) and turn(.) are specific propositional variables, called pseudofunction symbols, introduced in GDL for specifying a game rule. does(α) means that the action α is taken in this state. wins(a) means it is in a winning state of player a. turn(a) says it is player a's turn in the current state. The temporal formula ϕ is read as ϕ holds in the next stage of the game. All these language components are inherited from GDL.

The prioritised disjunctive connective ▽ is borrowed from [START_REF] Zhang | Representing and reasoning about game strategies[END_REF]. The formula ϕ 1 ▽ϕ 2 has to be read as "achieve ϕ 1 first; if it is impossible, achieve ϕ 2 ''. Different from [START_REF] Zhang | Representing and reasoning about game strategies[END_REF], we define the prioritised conjunction △ by the prioritised disjunction:

ϕ 1 △ ϕ 2 = def (ϕ 1 ∧ ϕ 2 )▽ϕ 1
It means "achieve both ϕ 1 and ϕ 2 ; if they are conflict, only achieve ϕ 1 ".

The two coalition operators [C] and [[C]

] are taken from ATL.

[C]ϕ says that coalition C has a joint strategy to achieve ϕ at the next state. [[C]]ϕ says that coalition C has a joint strategy for maintaining ϕ forever. From the semantics we will see that these operators are counterparts of C and C in ATL. To help the reader catch the intuition of the language, let us consider a special family of mnk-games [START_REF] Van Den Herik | Games solved: Now and in the future[END_REF].

Example 1. (mk-Game) An mk-game is a combinatorial game in which two players take turns in marking either a nought 'o' or a cross 'x' on an m × m board. The player who first gets k consecutive marks of her own symbol in a row (horizontally, vertically, or diagonally), will win the game. Obviously, an mk-game is a generalisation of Tic-Tac-Toe (m = k = 3) and Gomoku (m = 19 and k = 5). Now we describe the mk-games in our language. Given a player a ∈ {x, o}, let p a i,j denote that grid (i, j) is filled with player a's symbol, and α a i,j denote the action that player a fills grid (i, j) with her symbol, where 1 ≤ i, j ≤ m. The game rules can then be specified by the following formulas:

(1) initial → turn(x) ∧ ¬turn(o) ∧ m i,j=1 ¬(p x i,j ∨ p o i,j ) (2) wins(a) ↔ ( m i=1 m-k+1 j=1 k-1 l=0 p a i,j+l )∨ ( m-k+1 i=1 m j=1 k-1 l=0 p a i+l,j ) ∨( m-k+1 i=1 m-k+1 j=1 k-1 l=0 p a i+l,j+l ) ∨( m-k+1 i=1 m j=k k-1 l=0 p a i+l,j-l ) (3) teminal ↔ wins(x) ∨ wins(o) ∨ m i,j=1 (p x i,j ∨ p o i,j ) (4) does(α a i,j ) → ¬(p x i,j ∨ p o i,j ) ∧ turn(a) ∧ ¬terminal (5)
p a i,j ↔ p a i,j ∨ does(α a i,j ) ( 6) turn(a) → ¬turn(a) ∧ turn(-a), where -a represents a's opponent.

Statement [START_REF] Alur | Alternating-time temporal logic[END_REF] says that all grids are empty in the initial state and player x has the first turn. ( 2) and ( 3) specify the winning states for each player and terminal states for the game, respectively. ( 4) specifies the precondition of each action (legality). ( 5) is the combination of the frame axioms and effect axioms: a grid is marked with a player's symbol in the next state if the player takes the respective action in the current state or the grid has been filled before. The last formula specifies turn-taking.

State Transition Model

In order to provide the semantics for the logic, we use the state transition model to specify a game in the semantic level [START_REF] Zhang | Representing and reasoning about game strategies[END_REF].

Definition 1 (State Transition Model).

A state transition model M is a tuple (N, W, A, w, T, U, g, t, V ), where -N is a non-empty finite set of players; -W is a non-empty set of states; -A = a∈N A a where A a is a non-empty finite set of actions for agent a ∈ N .

w ∈ W is the initial state; -T ⊆ W is the set of terminal states; -U : A × W ֒→ W is a partial function specifying the state transitions.

g : N → 2 W is a goal function, specifying the winning states for each player;

-t : W \T → N is a label function, specifying players' turns. -V : W → 2 Φ is a standard valuation function.
To keep our formalism simple, we assume that all actions are performed asynchronously, and different players have different actions, i.e.,

A a ∩ A b = ∅ for any a = b ∈ N . Definition 2 (Complete Path). A sequence w 0 α 0 → w 1 α 1 → • • • α m-1 → w m is a complete path if 1. w 0 = w, w m ∈ T , and w i ∈ W for all 0 < i < m; 2. α i ∈ A for all 0 ≤ i < m; 3. U (w i , α i ) = w i+1 for all 0 ≤ i < m. Given a complete path δ = w 0 α 0 → w 1 α 1 → • • • α m-1
→ w m , we call the states w 0 , • • • , w m on δ reachable states. w j is the state at stage j. Let δ[i] be the i-th reachable state on path δ, and δ[i + 1] be the direct successor of δ[i] on δ. The set of all reachable states of δ is denoted by W δ . For each action a, we also let W a = {w ∈ W : t(w) = a} to denote the set of all states in which it is a's turn. Further more, we denote the set of all complete paths in a state transition model M as P(M ). Thus the set of all reachable states in M , denoted by W P(M) , is δ∈P(M) W δ .

A strategy for a player a is a plan of player a that determines what action she is to take at each reachable state when it is her turn. Formally, a strategy for player a is a total function f a : W a ∩ W P(M) → A such that U (w, f a (w)) is not undefined for all w ∈ W a ∩ W P(M) . A joint strategy for a coalition is a combination of its members' strategies. Formally, a joint strategy for a coalition

C ⊆ N is a total function f C : a∈C (W a ∩ W P(M) ) → A such that f C (w) = f a (w) if w ∈ W a . The set of all joint strategies of coalition C is denoted by F C .
Given a complete path δ and a non-terminal stage i (0 ≤ i < m) on δ, let σ(δ, i) denote the action taken at stage i on path δ. We say a complete path δ complies with player a's strategy

f a if for all w ∈ W a ∩ W δ , for all i ∈ N, if δ[i] = w, then σ(δ, i) = f a (w).
That is, for any reachable state w on δ where it is a's turn, the action taken at w on δ is the same as what the strategy f a specifies. Similarly, a complete path δ complies with a joint strategy

f C if for all w ∈ W a ∩ W δ , for all i ∈ N, if δ[i] = w, then σ(δ, i) = f C (w).
In fact, during game playing, a player often begins to use a strategy after reaching some game state. This means a complete path δ may start to comply with a joint strategy f C after reaching some state. Let P(f C , w) denote the set of complete paths δ reaching the state w at some stage i where the agents in C start to use the strategies f C . Formally,

P(f C , w) = {δ ∈ P(M ) | ∃i δ[i] = w and ∀j ≥ i σ(δ, j) = f C (δ[j])}

The Semantics

Before presenting the semantics for GDR, we need another notation. Let δ[0, i] denote the initial segment of path δ up to stage i. Any complete path λ that shares the same initial segment with δ up to stage i is denoted by δ[0, i] ⊑ λ. Given ϕ ∈ L, let

P(ϕ, δ[0, i]) = {δ ′ ∈ P(M ) | δ[0, i] ⊑ δ ′ and M, δ ′ , i |= ϕ}
denote the set of all complete paths that share the same initial segment of path δ up to stage i and satisfy ϕ at stage i. We are now in the position to give the truth conditions for GDR formulas.

Definition 3 (Truth Conditions

). Let M = (N, W, A, w, T, L, U, g, t, V ) be a state transition model. Given a complete path δ and a stage i on δ, we define the notion that ϕ ∈ L is true at i on δ, denoted by M, δ, i |= ϕ, as follows:

M, δ, i |= p iff p ∈ V (δ[i]) M, δ, i |= ¬ϕ iff M, δ, i |= ϕ M, δ, i |= ϕ 1 ∧ ϕ 2 iff M, δ, i |= ϕ 1 and M, δ, i |= ϕ 2 M, δ, i |= does(α) iff α = σ(δ, i) M, δ, i |= initial iff δ[i] = w M, δ, i |= terminal iff δ[i] ∈ T M, δ, i |= wins(a) iff δ[i] ∈ g(a) M, δ, i |= turn(a) iff t(δ[i]) = a M, δ, i |= ϕ iff M, δ, i + 1 |= ϕ M, δ, i |= ϕ 1 ▽ϕ 2 iff M, δ, i |= ϕ 1 , or (P(ϕ 1 , δ[0, i]) = ∅ and M, δ, i |= ϕ 2 ) M, δ, i |= [C]ϕ iff ∃f C ∈ F C ∀δ ′ ∈ P(f C , δ[i]) ∀j ∈ N if δ[i] = δ ′ [j], then M, δ ′ , j + 1 |= ϕ. M, δ, i |= [[C]]ϕ iff ∃f C ∈ F C ∀δ ′ ∈ P(f C , δ[i]) ∀j ∈ N if δ[i] = δ ′ [j], then ∀k ≥ j, M, δ ′ , k |= ϕ.
The interpretation for GDL components is straightforward. The last two statements define the semantical conditions for the coalition operators, which is similar to the ones in ATL. Assume that a path δ in a state transition model M diverges at stage i due to executing different actions as illustrated below:

δ i δ 1 α δ β δ 2 γ
Consider a formula does(α)▽does(β), which says "do action α; if α is not doable, do β". We check whether it is true at stage i on path δ. Since δ takes action β instead of α at i, we have M, δ, i |= ¬does(α) ∧ does(β). However, this does not mean α is not doable at i. In fact, it can be done through δ 1 (M, δ 1 , i |= does(α)) and δ 1 shares the same initial segment of δ up to stage i (i.e., δ 1 ∈ P(ϕ 1 , δ[0, i])). Thus α is doable at i. According to the semantics, M, δ, i |= does(α)▽does(β). This is because δ picks up β even though α is doable at state i.

It is worth noting that when i = m, we have M, δ, m |= does(α) for all α ∈ A, M, δ, m |= ϕ and M, δ, m |= [C]ϕ for all ϕ ∈ L. Given a state transition model M and a formula ϕ ∈ L, we say ϕ is globally true through a complete path δ, denoted by M, δ |= ϕ, if M, δ, i |= ϕ for all i on δ. ϕ is valid in model M , written as M |= ϕ, if M, δ |= ϕ for all complete paths δ ∈ P(M ). Furthermore, |= ϕ means that ϕ is valid in all state transition models.

Strategic Reasoning

We now show how to use our logical framework to reason about game strategies. We first formalise Johan Benthem's description of game-oriented principles and use them to derive two well-known results in combinatorial game theory.

Game-Oriented Principles

Johan Benthem described a number of game-oriented principles in his temporal forcing logic [START_REF] Van Benthem | Reasoning about strategies[END_REF]. These principles specify the fundamental properties of any finite games, and they can be formally presented and proved in our framework.

M |= ϕ ∧ [[∅]]((turn(a) ∧ ϕ → [N ]ϕ) ∧ b∈N \{a} (turn(b) ∧ ϕ → [∅]ϕ)) → [[a]]ϕ (A3) If C ∩ D = ∅, then M |= [[C]]φ ∧ [[D]]ψ → [[C ∪ D]](φ ∧ ψ) (A1
) is a fixed-point recursion, which says that to maintain a property for a whole game, a player must make sure it is true now and, before the game is terminated, either there is a strategy so that she can maintain the property at next step if it is his turn, or he can maintain the property at next step for all strategies of the player who is taking his turn. Note that the property under consideration must be state-wise (no time spanning). (A2) provides a sufficient condition for a player to construct a strategy that maintains a property. (A3) shows that strategic ability of disjoint coalitions is superadditive [START_REF] Pauly | A modal logic for coalitional power in games[END_REF].

It is easy to see that these three statements are the generalisation of Benthem's game-oriented principles (Fact 3: C1-C3 in [START_REF] Van Benthem | Reasoning about strategies[END_REF]). We formalise them and generalise them into the multi-agent case. Interestingly, the well-known results for two player games: weak determinacy and Zermelo's theorem are corollaries of the above theorem.

Proposition 1 (Weak Determinacy). Let M z be any state transition model for finite two-player games and N = {a, b}, then

M z |= [[a]](terminal → wins(a)) ∨ [[b]]¬[[a]](terminal → wins(a))
Weak determinacy says in any finite two-player game with perfect information either one player has a winning strategy or the other player has a strategy that ensures her opponent has no winning strategy.

Proposition 2 (Zermelo's Theorem).

M z |= [[a]](terminal → wins(a)) ∨ [[b]](terminal → wins(b)) ∨[[a]](terminal → T ie) ∨ [[b]](terminal → T ie)
where T ie = def (¬wins(a) ∧ ¬wins(b)).

Zermelo's theorem says in any finite two-player game with perfect information and three outcomes (win, lose and tie), at least one of the players has a strategy to win or to lead to a tie [START_REF] Polak | Backward induction: Chess, strategies, and credible threats[END_REF].

Strategy Representation

In this subsection, we discuss how to represent strategies in our language. We try to represent a strategy by a normal formula. We know that a strategy is player-specific and specifies a single action at each reachable state for a player when it is his turn. If there is a formula that satisfies this condition, this formula can then be a syntactical representation of a strategy for that player. This idea leads to the following definition. Definition 4. Given a state transition model M , a formula ϕ ∈ L is a strategy rule for player a if for all w ∈ W a ∩ W P(M) , A a (ϕ, w) = {α ∈ A a : ∃δ∃i M, δ, i |= ϕ, δ[i] = w and σ(δ, i) = α} is a singleton.

Obviously not every formula ϕ ∈ L can be a strategy rule. The main challenge is how to create a strategy rule from non-strategy rules (normal formulas). We borrow Zhang and Thielscher's idea to combine strategies using the prioritised strategy connectives [START_REF] Zhang | Representing and reasoning about game strategies[END_REF]. To demonstrate how they work, we use our running example.

Consider a simple mk-game where m = 5 and k = 3. After some practice or backward induction reasoning, we may find that the following simple ideas may help player x to win:

1. Fill the center. 2. If filling any grid leads to win, do it. 3. Fill a next (an empty grid next to her own symbol). 4. Fill any grid. 5. Try (1) first; if fails, try (2); if fails, try (3); if fails, do (4). These ideas can be formally represented in GDR language as follows (a ∈ {x, o}):

1. f ill center a = def does(α a 3,3 ) 2. attack a = def 5 j,k=1
(does(α a j,k ) ∧ wins(a))

3. f ill next a = def 5 j,k=1 p a j,k ∧ ( does(α a j-1,k ) ∨ does(α a j-1,k-1 ) ∨does(α a j-1,k+1 )∨
does(α a j,k-1 )∨does(α a j,k+1 )∨does(α a j+1,k-1 )∨does(α a j+1,k ) ∨does(α a j+1,k+1 ))2 4. f ill any a = def 5 j,k=1 does(α a j,k ) 5. combined a = def f ill center a ▽attack a ▽f ill next a ▽f ill any a It is easy to see that the formula combined a can be satisfied in any state when it is a's turn (due to f ill any a ). However, it is not a strategy rule because it can suggest more than one actions in one state. To make it to be a strategy rule, we need the following technical treatment.

Let B = {(i, j) : 1 ≤ i, j ≤ 5} be the game board and ≺ be the lexicographic order on B, i.e., [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF] [START_REF] Parikh | The logic of games and its applications[END_REF][START_REF] Parikh | The logic of games and its applications[END_REF]. For each grid ξ ∈ B, let c a ξ = (i,j)≺ξ does(α a i,j ), which represents the idea of player a to fill any grid from (1, 1) up to ξ. We let

≺ (1, 2) ≺ • • • ≺ (1, 5) ≺ (2, 1) ≺ • • • ≺
S a 53 = def (f ill center a ▽ attack a ▽f ill next a ▽ f ill any a ) △ c a (5,5) △ • • • △ c a (1,1)
Observation 1. Let M be the state transition model of 53-game. For any player a ∈ {x,o}, S a 53 is a strategy rule for player a.

Reasoning about Strategic Abilities of Game Players

In this subsection, we continue to use mk-games to demonstrate how to reason about strategic abilities of a player. A standard strategy stealing argument from combinatorial game theory shows that there is no winning strategy for the second player in any mk-game. This can be easily described as follows: Proposition 3. Let M mk be any state transition model for mk-games. Then

M mk |= ¬[[o]](terminal → wins(o))
By Proposition 2, we derive that the first player x has a no-losing strategy:

M mk |= [[x]](terminal → ¬wins(o))
According to Observation 1, S a 53 is a strategy rule for player a. We now prove that this is actually a winning strategy for the player who has the first move in 53-game. To this end, we say that a state transition model M complies with player a's strategy f a specified by a strategy rule S a , denoted by M S a , if for all complete paths δ ∈ P(M ), δ complies with f a . Formally, P(M S a ) = {δ ∈ P(M ) : M, δ |= turn(a) → S a }. With this notion, we can reason about that the strategy specified by S x 53 is a winning strategy for player x in 53-game. Observation 2. For all δ ∈ P(M S x 53 ), M 53 , δ |= terminal → wins(x)

This is just a simple example. In fact, our language can be used to describe more complicated strategies for more complicated games. We have provided a constructive approach to show Tic-tac-toe game can be forced in a draw. Currently we are working on the logical description of the winning strategy for Gomoku game, invented by Allis et al. [START_REF] Allis | Go-moku solved by new search techniques[END_REF][START_REF] Allis | Proof-number search[END_REF], and formally prove it to be a winning strategy instead of the computer assisted proof [START_REF] Allis | A knowledge-based approach of connect-four[END_REF][START_REF] Allis | Searching for solutions in games and artificial intelligence[END_REF][START_REF] Wágner | Solving renju[END_REF].

Model Checking

The model-checking problem for GDR is the problem of determining: for a given GDR formula ϕ, a state transition model M , a complete path δ and a stage i in M , whether or not M, δ, i |= ϕ. By establishing a translation from GDR to ATL ⋆ , we show an upper bound of the model-checking problem for GDR, which is no worse than the model-checking problem for ATL ⋆ .

From GDR Model to ATL ⋆ Model

In this part, we will show any state transition model can be transformed into a ATL ⋆ model, using the methods in [START_REF] Ruan | Verification of games in the game description language[END_REF]. The main idea is that we encode notions like terminal, turn, wins through valuation π, rather than through separate relations or functions. For this purpose, we redefine the set of atomic propositions of GDR, denoted by At GDR , as follows:

At GDR = def Φ ∪ {terminal} ∪ {turn(a), wins(a) | a ∈ N }
Given a state transition model M = (N, W, A, w, T, U, g, t, V ) and a set of atomic propositions At GDR , we define an associate action-based alternating transition system(AATS) done(α) ∈ Φ ′ for all α ∈ i∈N A ′ i representing actions that are done in the transition from previous state to current state3 .

T M = {W ′ , w, N, A ′ 1 , • • • , A ′ n , ρ, τ, Φ ′ ,
initial ∈ Φ ′ and s ⊥ ∈ Φ ′ where s ⊥ is a special atom to specify a 'sink state' which is the only successor of a terminal state and itself.

The other components of T M are constructed as follows:

With this, we have the following correspondent result between the state transition model and its associated AATS with respect to the translation. Lemma 1. Given a state transition model M , a complete path δ in M and a stage i on δ, for any GDR formula ϕ ∈ L,

(1) if ST ⋆ (ϕ) is an ATL ⋆ state formula, M, δ, i |= GDR ϕ iff T M , δ[i] |= ATL ⋆ ST ⋆ (ϕ); (2) if ST ⋆ (ϕ) is an ATL ⋆ path formula, M, δ, i |= GDR ϕ iff T M , δ[i, ∞] |= ATL ⋆ ST ⋆ (ϕ).
It follows that the model-checking problem for GDR is no more complicated than ATL ⋆ . Since the model-checking problem for ATL ⋆ is 2EXPTIME-complete [START_REF] Alur | Alternating-time temporal logic[END_REF], then we have the following result.

Theorem 2. The model-checking problem for GDR is in 2EXPTIME.

Conclusion

We have presented a unified logical framework for game description, strategy representation and strategic reasoning. The language of the framework combines GDL, ATL and prioritised strategy connectives. To minimize the complexity of this language, we took a cautious way of doing that. We do not introduce until operator U and legal(). We have demonstrated that our language is rich enough to express generic game results such as Weak Determinacy and Zermelo's Theorem as well as complicated game strategies. Most of the related work has been discussed in the introduction. Besides that, the following is also worth mentioning.

Ruan et al. studied the relationship between GDL and ATL [START_REF] Ruan | Verification of games in the game description language[END_REF]. Different from our motivation, their goal is to use ATL to reason about GDL-specified games. Therefore, instead of integrating language components, they focus on how to transfer a GDL game specification into an ATL specification.

We would also like to mention that there are three essential differences between Zhang and Thielscher's work [START_REF] Zhang | Representing and reasoning about game strategies[END_REF] and ours. Firstly, their definition of the prioritized connectives was based on the semantics of strategies rather than on the semantics of the logic. Strictly speaking, their prioritized connectives are not part of their logical language. However, our ones are part of the logical language. Secondly, we define these connectives as binary operators while theirs are multiple tuple operators. The prioritized conjunction operators diverge when arguments are more than two due to non-associativity. Thirdly, their work does not have the facility for reasoning about strategic abilities of players.

There are many directions for future investigations. Firstly, our approach may be used in the development of general game players. Since GDL is the native language for general game playing, with further extension of prioritised strategy connectives, a player would be able to combine simple actions into more complicated actions. Secondly, with our approach we may be able to provide logical solutions for already solved games, such as Connect Four and Gomoku, instead of the computer assisted solutions [START_REF] Allis | A knowledge-based approach of connect-four[END_REF][START_REF] Allis | Searching for solutions in games and artificial intelligence[END_REF][START_REF] Wágner | Solving renju[END_REF]. With the help of model-checking approach, we may be also develop solutions for some unsolved games. Moreover, it would be interesting to investigate the epistemic extension of the current framework so as to study the beliefs of other players' strategies.

  [C]ϕ (or [[C]]ϕ) is true if coalition C has a joint strategy to make ϕ true in the next stage (or maintain ϕ from now on) for all possible complete paths in the set P(f C , δ[i]) Note that index j denotes the stage when complete path δ ′ reaches the state δ[i]. It is possible that i = j, since two paths may reach the same state at different stages. To show the interpretation of the prioritised disjunction ▽, let's consider the following example.

Theorem 1 .

 1 For any state transition model M , a ∈ N , C, D ⊆ N and ϕ, φ, ψ ∈ L, (A1) If ϕ does not contain and does(.), then M |= [[a]]ϕ ↔ ϕ∧(terminal∨(turn(a)∧[N ][[a]]ϕ)∨ b∈N \{a} (turn(b)∧[∅][[a]]ϕ)) (A2) If ϕ does not contain and does(.),

  π} with the same set of agents N = {1, • • • , n} and initial state w, and such that Φ ′ is constructed in the following manner. Definition 5. Define a translation ST: At GDR → At ATL ⋆ associating every atom in At GDR with an atom in AT AT L * : ST(turn(a)) = turn(a) ST(wins(a)) = wins(a) ST(terminal) = terminal ST(p) = p for all p ∈ Φ Then we next define the set of atomic propositions Φ ′ as a set of atoms such that for all p ∈ At ATL ⋆ , p ∈ Φ ′ .

The other logical connectives ∨, →, ↔ and constants ⊤, ⊥ can be defined in the standard way.

To avoid too much complexity, we ignore the cases when the indexes go over their range.

Note this concept as well as the following two concepts sink state and f in i is borrowed from[START_REF] Ruan | Verification of games in the game description language[END_REF].

-ST ⋆ (p) = ST(p) for all p ∈ At GDR -ST ⋆ (initial) = initial -ST ⋆ (¬ϕ) = ¬ST ⋆ (ϕ) -ST ⋆ (ϕ 1 ∧ ϕ 2 ) = ST ⋆ (ϕ 1 ) ∧ ST ⋆ (ϕ 2 ) -ST ⋆ (does(α)) = done(α) -ST ⋆ (ϕ 1 ▽ϕ 2 ) = ST ⋆ (ϕ 1 )∨( ∅ ¬ST ⋆ (ϕ 1 ) ∧ ST ⋆ (ϕ 2 )) -ST ⋆ ( ϕ) = (¬s ⊥ → ST ⋆ (ϕ)) -ST ⋆ ([C]ϕ) = C (¬s ⊥ → ST ⋆ (ϕ)) -ST ⋆ ([[C]]ϕ) = C (✷)(¬s ⊥ → ST ⋆ (ϕ))

-W ′ = W 1 ∪ W 2 where W 1 = W and W 2 = {s w | w ∈ W 1 } including sink states.

-A ′ i = A i ∪ {noop i } ∪ {f in i } where for all 1 ≤ i ≤ n A i is the same as that in M , noop i means player i does nothing, and f in i is an action for the terminal and sink states ρ

where

is a valuation function such that for any w ∈ W ′ π(w) is a set of atoms satisfying the following conditions:

(1) for all w ∈ W 1 ,

• for any p ∈ Φ, p ∈ V (w) iff p ∈ π(w);

• w ∈ T iff terminal ∈ π(w);

• for any a ∈ N , t(w) = a iff turn(a) ∈ π(w);

• for any a ∈ N , w ∈ g(a) iff wins(a) ∈ π(w);

Given a complete path δ in M , we extend δ to an infinite path (computation) in T M with the sink state labelled by the terminal state of δ. We denote it by δ. We use δ[i, ∞] to denote the infinite subsequence of δ starting at stage i.

Translation from GDR to ATL ⋆

We next define a translation map from GDR formulas to ATL ⋆ formulas to make GDR embedded into ATL ⋆ . Definition 6. A translation ST ⋆ from GDR formulas to ATL ⋆ formulas is defined as follows: