Alternating Epistemic Mu-Calculus

1 Introduction

Alternating-time temporal logic (ATL) [2] is probably the most popular logic that allows reasoning about agents' abilities in strategic encounters. ATL combines features of temporal logic and basic game theory, which are both encapsulated in the main language construct of the logic, 〈〈A〉〉γ, which can be read as "the group of agents A has a strategy to enforce γ", where γ is a temporal property including operators © ("next"), ✷ ("always") and/or U ("until"). ATL was originally proposed for reasoning about agents in perfect information scenarios. Since then, several variations have been studied for imperfect information [9; 7; 1; 5; 8]. One of the features that distinguishes them from the perfect information setting is that the fixed point characterizations of temporal modalities do not hold anymore under imperfect information. On the conceptual level, this means that having a strategy to achieve ϕ does not mean that the agents will be able to recompute the strategy when they are already executing it. Thus, the semantics of these ATL variants includes an implicit assumption that agents can remember the strategy which they are executing even if they forget everything else.

Wojciech Jamroga

Computer Science and Communication, University of Luxembourg

wojtek.jamroga@uni.lu

This can be a good thing or a bad thing, depending on the notion of ability that one wants to formalize. Nevertheless, the other kind of ability (enforcing ϕ without resorting to additional memory of the strategy) is at least as important. It captures the idea of agents "persistently knowing how to play to enforce ϕ", i.e., so that they can come up with the right strategy not only at the beginning of the game; they will know how to recreate the strategy also in any future moment of the play. Moreover, this kind of ability has a minimalistic flavor regarding epistemic prerequisites: agents are supposed to achieve ϕ while resorting only to observations that they can make along the way.

In this paper, we argue that this class of abilities cannot be expressed in the existing variants of ATL. We also propose that, instead of considering yet another semantics of strategic operators, it suffices to add explicit fixed point operators to the "next-time" fragment of ATL. In terms of technical results, our contribution is threefold: (1) We show that the new logic is incomparable with "ATL with imperfect information" regarding expressive power. (2) We propose specifications of natural types of strategic abilities. (3) We point out that verification of such abilities can be cheaper than for all the variants of "ATL with imperfect information" considered so far.

Recomputable strategies are ones that do not have to be remembered by the agents in order to execute them. In a sense strategies of this kind impose the weakest requirements on agents' memory. Moreover, recomputable strategies can be (by definition) synthesized incrementally, which can make the synthesis tractable-at least for small coalitions.

2 Agent Logics: Preliminaries

In this section we provide a brief overview of existing variants of alternating-time temporal logic (ATL) in the way they were proposed in [2] and later refined in [9]. Finally, we recall the definition of alternating μ-calculus (AMC) which was introduced in [2].

2.1 Concurrent (Epistemic) Game Structures

The semantics for the logics are defined over a variant of transition systems where transitions are labeled with combinations of actions, one per agent. An imperfect information concurrent game structure (ICGS) [10; 9] is given by M = 〈Agt,Q, Π, π,Act, d, o, {∼a| a ∈ Agt}〉 which includes a nonempty finite set of all agents Agt = {1, . . . , k}, a nonempty set of states Q, a set of atomic propositions Π and their valuation π : Π → P(Q), and a nonempty finite set of (atomic) actions Act. Function d : Agt × Q → P(Act) defines nonempty sets of actions available to agents at each state, and o is a (deterministic) transition function that assigns the outcome state q′ = o(q, α1 , . . . , αk) to state q and a tuple of actions 〈α1 , . . . , αk〉 for αi ∈ d(i, q) and 1 ≤ i ≤ k, that can be executed by Agt in q. We write da(q) instead of d(a, q). Each ∼a⊆ Q × Q is an equivalence relation satisfying da(q) = da(q′ ) for q ∼a q′ . These relations model incomplete information in the way it is done in epistemic logic. Note that the perfect information models from [2] (CGS, concurrent game structures) can be modeled by assuming each ∼a to be the minimal reflexive relation.

A strategy of agent a is a conditional plan that specifies what a is going to do in each situation. A natural taxonomy of four strategy types was introduced in [9] and labeled as follows: i (resp. I) stands for imperfect (resp. perfect) information, and r (resp. R) refers to imperfect (resp. perfect) recall. The following types of strategies can be used in the respective semantic variants:

• Ir: sa : Q → Act such that sa(q) ∈ da(q) for all q (agents have perfect information and base their decisions on states only);
• IR: sa : Q + →Act such that sa(q0 . . . qn) ∈ da(qn) for all q0 . . . qn (agents have perfect information and base their decisions on the whole history of events happened);
• ir: like Ir, with the additional constraint that q ∼a q′ implies sa(q) = sa(q′ ) (agents have to assign the same choice to states which appear indistinguishable to them);
• iR: like IR, with the additional constraint that h ≈a h′ implies sa(h) = sa(h′ ), where ≈a encodes indistinguishability of histories as follows. For h = q0 q1 . . . qn ∈ Q + and h′ = q′0 q′1 . . . q′n′ ∈ Q + we have h ≈a h′ iff n = n′ and qi ∼a q′i for i = 1, . . . , n.

A collective xy-strategy sA is a tuple of xy-strategies, one per agent fromA, for xy = Ir, IR, ir, iR. Additionally, sA|a denotes agent a's part of collective strategy sA. The set of A's collective xy-strategies is defined as Σxy A .

A path λ = q0 q1 q2 . . . is an infinite sequence of states such that there is a transition between each qi, qi+1. We use λ[i] to denote the ith position on path λ (starting from i = 0) and λ[i,∞] to denote the subpath of λ starting from i.

Function outM(q, sA) returns the set of all paths that can result from the execution of strategy sA from state q in model M, see [2] for the precise definition. We define outxy M (q, sA) = outM(q, sA) for xy = Ir, IR, and outxy M (q, sA) = ⋃a∈A ⋃q∼aq′ outM(q′ , sA) for xy = ir, iR.

2.2 Alternating Time Temporal Logic

The language LATL (Π,Agt) is given by the following grammar [2]:

ϕ ::= p | ¬ϕ | ϕ∧ϕ | 〈〈A〉〉 ©ϕ | 〈〈A〉〉✷ϕ | 〈〈A〉〉ϕUϕ where A ⊆ Agt and p ∈ Π. Additionally, we define "sometime in the future" as ✸ϕ ≡ ⊤Uϕ.

Using xy-strategies defined above we obtain the logics ATLxy for x ∈ {i, I} and y ∈ {r,R}. The xy-semantics, |=xy, is defined by the following clauses where we omit the standard cases for propositions, negation, and conjunction:

• M, q |=xy 〈〈A〉〉©ϕ iff there is a collective xy-strategy sA such that, for each λ ∈ outxy (q, sA), M, λ[1] |=xy ϕ;
• M, q |=xy 〈〈A〉〉✷ϕ iff there is an xy-strategy sA s.t., for each λ ∈ outxy (q, sA) and every i ≥ 0, M, λ[i] |=xy ϕ;
• M, q |=xy 〈〈A〉〉ϕUψ iff there is an xy-strategy sA s.t., for each λ ∈ outxy (q, sA), there is i ≥ 0 for which M, λ[i] |=xy ψ, andM, λ[j ] |=xy ϕ for each 0 ≤ j < i.

Informally speaking, M, q |= 〈〈A〉〉γ iff, there exists a collective strategy sA such that γ holds on all outcome paths that the agents in A consider possible executions of sA. Moreover, in the ir- and iR-semantics, we can define knowledge operators Kaϕ as 〈〈a〉〉ϕUϕ and we define the "everybody in A knows" modality EA as ∧a∈A Ka. It is easy to check that M, q |=xy Kaϕ iff for all q′ with q ∼a q′ , M, q′ |=xy ϕ, for xy = ir, iR.

Note that M, q |=ix 〈〈A〉〉γ requires A to have a single strategy that is successful in all states indistinguishable from q for any member of the coalition.

2.3 AlternatingMu-Calculus

Alternating μ-calculus (AMC) replaces the temporalstrategic operators 〈〈A〉〉✷, 〈〈A〉〉U with the least fixed point operator μ. Like the basic version of ATL, AMC was proposed in the context of perfect information scenarios. The language LAMC (Π, Agt, Var) is given by the following grammar [2]:

where A ⊆ Agt, p ∈ Π, X ∈ Var and each ϕ in μX(ϕ) is X-positive, i.e. each free occurrence of X in ϕ is under the scope of an even number of negations in ϕ. We define νX(ϕ(X)) as ¬μX(¬ϕ(¬X)) where ϕ(¬X) is equivalent to ϕ(X) but each free occurrence of X in ϕ is replaced by ¬X. We also take [A]ϕ as ¬〈A〉¬ϕ and define conjunction in the standard way. Var is the set of fixed point variables, i.e., second order variables ranging over sets of states.

Here we consider only the alternation-free fragment of AMC. The corresponding language Laf-AMC (Π,Agt, Var) consists of all alternation-free formulae of LAMC (Π, Agt, Var); i.e. all formulae of which their positive normal form (i.e. negations occur only in front of propositions) contains no occurrences of ν (resp. μ) on any syntactic path from an occurrence of μX (resp. νX) to a bound occurrence of X (cf. [2]).

A (Var,Q)-valuation V is a mapping V : Var → P(Q). Given a variable X and a set Z ⊆ Q of states we define V [X := Z ](Y ) = {V(Y ) if X ̸= Y ; Z else. That is, the valu-

ation V[X := Z ] equals V for all variables different from X and assigns Z to X. The semantics for LAMC is given by the denotation function [[·]]MV that maps LAMC -formulae to sets of states (i.e. [[ϕ]]MV ⊆ Q) where M is a CGS and V is a valuation. The denotation function is defined as follows: [[p]]MV = π(p), [[X]]MV = V(X), [[¬ϕ]]MV = Q\[[ϕ]]MV , [[ϕ ∧ ψ]]MV = [[ϕ]]MV ∩ [[ψ]]MV , [[〈A〉ϕ]]MV = {q | ∃αA ∈ dA(q)∀αAgt\A ∈ dAgt\A : o(q, (αA, αAgt\A)) ∈ [[ϕ]]MV }, and [[μX(ϕ)]]MV = ⋂{Z ⊆ Q | [[ϕ]]MV[X:=Z] ⊆ Z}.

Finally, we write M, q |=V ϕ for q ∈ [[ϕ]]MV and M, q |= ϕ if M, q |=V ϕ for all (Var,Q)-valuations V. We omit "(Var,Q)" if clear from context.

2.4 Known Expressivity Results

Definition 1 (Comparing expressivity) A logic L1 is as expressive as L2 over a class of models M (written L2 ⪯M L1) iff there is a translation TR of L2 formulae to L1-formulae such that for each L2-formula ϕ we have: M |=L2 ϕ iff M |=L1 TR(ϕ) for all M ∈M.

We say that L1 is more expressive than L2 (L2 ≺M L1) iff L2 ⪯M L1 but not L1 ⪯M L2. Finally, we call L1 , L2 incomparable if neither L2 ⪯M L1 nor L1 ⪯M L2.

We note, that for two classes of models M and M′ with M⊆M′ , if not L2 ⪯M L1 then also not L2 ⪯M′ L1.

The following translation TRATLIR (·) : LATL → Laf-AMC shows how LATL -formulae can be encoded into Laf-AMC [2]: TRATLIR (p) = p, TRATLIR (¬ϕ) = ¬TRATLIR (ϕ), TRATLIR (〈〈A〉〉©ϕ)=〈A〉TRATLIR (ϕ), TRATLIR (〈〈A〉〉✷ϕ) = νX(TRATLIR (ϕ) ∧ 〈A〉X), and TRATLIR (〈〈A〉〉ϕ1Uϕ2) = μX(TRATLIR (ϕ2) ∨ (TRATLIR (ϕ1) ∧ 〈A〉X)).

Proposition 1 ([2]) For all LATL -formulae ϕ, all CGS M and all states q ∈ QM we have: M, q |=ATLIR ϕ iff M, q |=af-AMC TRATLIR (ϕ).

Theorem 2 ([2]) Alternation-free AMCIr is more expressive than ATLIR.

3 Alternating Epistemic Mu-Calculus

Alternating μ-calculus was introduced for reasoning about systems in which agents always know the current state of affairs. To the best of our knowledge, analogous logics have never been considered for systems with imperfect information. In this section we propose an imperfect information semantics for Laf-AMC in a straightforward way. The only change concerns the semantic clause for operator 〈A〉. Now, 〈A〉ϕ is only true if agents A have a collective onestep strategy which enforces ϕ from all the states that are indistinguishable from the current one. Also, since knowledge operators Ka cannot be expressed anymore when the "until" operator is missing, we add them explicitly to the language. This way, we obtain the alternation-free alternating epistemic μ-calculus, af-AMCi in short.

3.1 Syntax and Semantics

Definition 2 (Laf-AMCi ) The language LAMCi (Π,Agt, Var) extends the definition of LAMC by formulae Kaϕ; that is, it is defined by the grammar:

where A ⊆ Agt, a ∈ Agt, p ∈ Π, X ∈ Var and each ϕ in μX(ϕ) is X-positive, as before. Additionally, to the macros defined above we define "everybody in A knows" as EAϕ = ∧a∈A Ka and ˆKaϕ = ¬Ka¬ϕ. Analogously to the perfect information case, we define the alternation-free sublanguage Laf-AMCi (Π, Agt, Var) of LAMCi (Π, Agt, Var).

Definition 3 (Imperfect information semantics) Let M be an ICGS and V a valuation of fixed point variables. The isemantics for Laf-AMC (Agt, Π, Var)-formulae, denoted [[·]]Mi,V , is defined as the semantics [[·]]MV (the modification to ICGSS is straightforward) extended with the following semantic clauses:

In other words, q ∈ [[〈A〉ϕ]]Mi,V iff agents A have a collective ir-strategy such that everybody in the group knows that it enforces ϕ in the next step.

We write M, q |=i ϕ iff q ∈ [[ϕ]]Mi,V for all valuations V of fixed point variables from Var.

Example 1 Consider the ICGS M shown in Figure 1. The story is as follows: A married man is sitting in a pub drinking with his friends (q0). In order to get back to his wife (q2), he needs to finish his drinking session first (q1), but that will result in a temporary lapse of memory. In particular, the man can have a nagging feeling that something might be wrong with his marriage, e.g. his wife could have left him because of his drinking habits (q′1 ), in which case he can only come back to an empty house (q′2 ).

Trivially, we have that M, q0 |=ir 〈〈1〉〉✸p, so the man should rest assured. However, is it really the property he is after? He knows now that everything will be fine, but he also know that he will get confused on the way, which may prevent him from reaching his goal. The stronger kind of ability is captured by the af-AMCi formula μX(p ∨ 〈1〉X), which is not true inM, q0.

The example suggests that ATLir and af-AMCi offer means to refer to different types of strategic ability.

We proceed with this issue in Section 3.2, where we show that both logics are incomparable, and in Section 4, where we analyse the new kind of strategic ability.

3.2 Expressivity

We start by showing that, like in the perfect information setting, af-AMCi still allows to capture properties that cannot be expressed in ATLir.

Proposition 3 ATLir is not as expressive as af-AMCi over the class of ICGSS.

Proof. It is known that the alternation-free modal μ-calculus (af-MC) is strictly more expressive than CTL over the class MK of Kripke structures. That is, for any translation of af-MC-formulae to CTL-formulae there is a af-MC-formula ϕ such that not MK |=af-MC ϕ iff MK |=CTL T RCTL(ϕ).

Now suppose ATLir were af-AMCi-expressive over the class of ICGSS. Then, ATLir would also be af-AMCiexpressive over MK as MK can be seen as the class of perfect information single agent ICGSS. Thus, CTL would also be af-MC-expressive over MK . Contradiction. ■

Note that we do not use epistemic operators in the proof, so they are not the reason for the expressivity gap.

The other direction is more surprising. First, we show that naive ideas for a translation from ATL to af-AMC in the imperfect information setting do not work.

Proposition 4 There is an LATL -formula ϕ, an ICGS M, and a state q ∈ QM such that: M, q |=ATLir ϕ and M, q ̸|=af-AMCi TRATLIR (ϕ).

Proof. Consider model M from Figure 1 and the ATL formula ϕ ≡ 〈〈1〉〉✸p. Now, TRATLIR (ϕ) = μX(p ∨ 〈1〉X). It is easy to see that M, q0 |=ir ϕ but M, q0 ̸|=i TRATLIR (ϕ). ■

We may try to repair the translation by use of epistemic operators that take into account also states indistinguishable from the current one. Let the epistemic extension TRATLiR (·) of the standard translation TRATLIR (·) be obtained by modifying the standard translation as follows. For every LATL - formula ϕ = 〈〈A〉〉ψ we set TRATLiR (ϕ) = EATR∗ATLiR (ϕ) where TR∗ATLiR (·) is defined as TRATLIR (·) but each nested occurrence of TRATLIR (·) is replaced by TRATLiR (·). We will refer to TRATLiR (·) as epistemic standard translation.

Proposition 5 There is an LATL -formula ϕ, an ICGS M, and a state q ∈ QM such that: M, q |=ATLir ϕ and M, q ̸|=af-AMCi TRATLiR (ϕ).

Proof. Again, we use the model M from Figure 1 and ϕ ≡ 〈〈1〉〉✸p. TRATLiR (ϕ) = E1μX(p ∨ 〈1〉X). Now, we have again that M, q0 |=ir ϕ but M, q0 ̸|=i TRATLiR (ϕ). ■

So, is there another translation that gives us the desired characterisation? The next results show that such a translation does not exist. Due to lack of space we omit the full proofs.

Proposition 6 af-AMCi is not as expressive as ATLir over the class of ICGSS.

Proof. (Idea) The basic idea is that the ATLir-formula 〈〈1〉〉✸p does distinguish the models M and N in state q0 shown in Fig. 1 but there is no af-AMCi-formulae which can. ■

The next theorem follows from Propositions 3 and 6.

Theorem 7 af-AMCi is incomparable to ATLir in expressive power over the class of ICGSS.

How does the picture change if agents have memory? That is, we compare ATLiR and af-AMCi. (Note that it does not make sense to consider memory in af-AMCi since the strategic modalities refer only to one-step strategies there.) Clearly, Proposition 6 holds for ATLiR. But also Proposition 3 holds, since ATLiR and ATLir are equally expressive over (pure) CGSS. Hence, if the analogous result were not true ATLiR would also be at least as expressive as af-AMCi over singleagent CGSS. As before this yields a contradiction, for af-MC is known to be strictly more expressive than CTL.

Theorem 8 af-AMCi is incomparable to ATLiR in expressive power over the class of ICGSS.

4 Specification and Verification of Abilities

In this section we argue that af-AMCi can be useful for specifying and verifying meaningful strategic properties of agents. We begin with a formalization of the intuitions we tried to convey in the introduction. To this end, we define fixed point properties that formally capture those informal intuitions.

4.1 Strategic Fixed Points: Achievement

The main intuition behind our proposal is that we enable expressing that agents A have a strategy to enforce a temporal property γ while knowing how to play all along the game. For achievement properties, we have typically γ ≡ ✸ϕ. We note that the ability to eventually achieve ϕ while knowing how to play all along can have at least two meaningful interpretations:

1. A have a strategy which they know to achieve ϕ, can be recomputed along the execution, and guarantees that they will know when ϕ has been achieved;
2. The agents have a recomputable strategy that they know to achieve ϕ, but they will not necessarily know when ϕ is achieved.

For a single agent the first achievement ability corresponds closely to the af-AMCi-formula:

We observe that this formula (and formulae of af-AMCi in general) has a strong "constructive" flavor. For example, the given formula requires not only that a has a uniform strategy to eventually obtain p, but also that

• she can recompute the strategy at any future state resulting from executing it,
• she knows about this; and furthermore,
• with every step, a knows that the goal is closer, and hence the part of the strategy that she needs to recompute becomes smaller.

This is a stronger kind of ability than those typically expressed in ATLir. For illustration, consider model M1 in Figure 2. Agent a has a uniform strategy to achieve p eventually: M1 , q0 |= 〈〈a〉〉✸p (the strategy is to play α everywhere). It is even the case that a can recompute a successful strategy on the way (M1 , q0 |= 〈〈a〉〉(〈〈a〉〉✸p)Up)-which is trivial as only a single action is available. However, the afAMCi-formula does not hold: M1 , q0 ̸|= μX(Kap ∨ 〈a〉X). This is because a is never certain that the goal state is really approaching. More precisely, suppose a executes α in state q0. In the next state, q1, she executes α again. However, as she considers q3 possible the resulting state could-from her perspective-also be q0. Applying this reasoning iteratively a possible execution path could also be q0 q3(q0 q3)ω which does never satisfy p. Hence, the agent does not know to have a recomputable strategy to achieve p.

Analogously, we can also describe the second interpretation of the achievement property by

We omit the formal characterizations due to lack of space. We note also that the relationships for proper coalitions are more sophisticated; the exact study is left for future work.

4.2 Strategic Fixed Points: Maintenance

In this section we turn to maintenance properties. They are typically expressed by ✷ϕ. Like for achievement properties, the ability to maintain ϕ while knowing how to play all along can have at least two interpretations:

1. A have a strategy to maintain ϕ and keep knowing that ϕ, that can be recomputed at every step.
2. The agents have a recomputable strategy to maintain ϕ (but they may be unsure if ϕ is true at some steps).

Similar to the case of achievement properties we can describe the first property by

In this his case the difference between ATLir and afAMCi specifications is perhaps even clearer. As an example we consider model M2 shown in Figure 2. We have M2 , q0 |= 〈〈a〉〉✷¬p which expresses that a can avoid p. For example, take the strategy in which α is played everywhere. We even have M2 , q0 |= 〈〈a〉〉✷〈〈a〉〉✷¬p (while avoiding p, she can recompute a successful strategy). However, at q1, a can only come up with a strategy that is different from the original strategy (i.e., play β everywhere), and indeed M2 , q0 ̸|= νX(Ka¬p ∧ 〈a〉X).

Again, the second property can be described in a similar way by formula

Combinations of achievement and maintenance, captured by the "until" operator U, can be treated analogously.

4.3 Verification

In the previous sections we have shown that af-AMCi allows to specify interesting properties that cannot be expressed in the existing variants of ATL for imperfect information. A natural question arises: How costly is the verification of these properties? It is known that:

• Model checking of strategic logics of perfect information (ATLIr, ATLIR, af-AMC) is in P [2];
• Verification of ATLir (imperfect information and memoryless strategies) is ΔP2 -complete even for turn-based systems consisting of a single agent [9; 6];
• Model checking ATLiR (imperfect information, perfect recall) is undecidable [4].

Here, we show that model checking the alternating μcalculus under imperfect information is in P for coalitions consisting of at most two agents (in a system including arbitrarily many agents). Moreover the problem is between NP and ΔP2 if larger coalitions are involved. Thus, verification with af-AMCi can be distinctly cheaper than with ATL for abilities of small coalitions, and no harder in the general case.

First, we point out that the μ-operator in af-AMCi is a standard least fixed point operator. Thus, the crucial part of model checking is the computation of the preimage for 〈A〉 (i.e., the set of states satisfying 〈A〉p for a given proposition p). Then, verification of an arbitrary formula can be done through a polynomial number of calls to preimage computations within the standard iterative algorithm (cf. e.g. [3]). The complexity of the preimage computation turns out to be as follows.

Proposition 9 Checking if M, q |= 〈A〉p for |A| ≤ 2 can be done in linear time wrt the number of transitions inM.

Proof. The algorithm for A = {a1 , a2} is given below. It is easy to see that it never processes the same transition twice.

Let Q = [q]∼A and D = da1 (q) × da2 (q);

while there is still a collective action (α1 , α2) in D do:

• Fix α1 for a1 in [q]∼a1 and α2 for a2 in [q]∼a2 .
• For every state in [q]∼A there is at most one agent in A for whom the action has not been fixed. If ai's action is not fixed for q′ , q′′ such that q′ ∼ai q′′ then collapse q′ , q′′ into a single state (taking the union of the outgoing transitions). Repeat iteratively;
• If in the resulting perfect information ICGS A have a one-step strategy to enforce p in the next state then return true else remove (α1 , α2) fromD and revert to the original model M;

If the loop ended with no success, there are no more available actions, so return false. ■

Proposition 10 Model checking 〈A〉p in M, q is in NP wrt. the number of transitions inM.

Proof. (Sketch) Guess a one-step strategy of A, remove from M the irrelevant transitions and states outside [q]∼A , and check if p holds for all the remaining "next" states. ■

Proposition 11 Model checking 〈A〉p in M, q for |A| ≥ 3 is NP-hard wrt. the number of transitions inM.

Proof. (Sketch) We use an adaptation of the SAT reduction from [6]. Given a Boolean formula Φ in CNF, we construct a 3-agent ICGS MΦ as follows. Each literal l from clause ψ in Φ is associated with a state qψ l . At state qψ l , player 1 indicates a literal from ψ, and player 2 decides on the valuation of the underlying Boolean variable. If 1 indicated a "wrong" literal l′ ̸= l then the system proceeds to state q⊤ where proposition yes holds. The same happens if 1 indicated the "right" literal (l) and 2 selected the valuation that makes l true. Otherwise the system proceeds to the "sink" state q⊥.

Player 1 must select literals uniformly within clauses, so qψ l ∼1 qψ′ l′ iff ψ = ψ′ . Player 2 is to select uniform valuations of variables, i.e., qψ l ∼2 qψ′ l′ iff var(l) = var(l′ ) where var(l) is the variable contained in l. Finally, all states except q⊤, q⊥ are indistinguishable for 3. An example of the construction is presented in Figure 3.

Then, Φ is satisfiable iff MΦ, q |= 〈1, 2, 3〉yes where q is an arbitrary "literal" state. ■

The following is a straightforward corollary (We conjecture that it is actuallyΔP2 -complete.).

Theorem 12 Model checking af-AMCi for formulae that include only operators 〈A〉 with |A| ≤ 2 can be done in polynomial time wrt. the size of the model and the length of the formula. In general, the problem is NP-hard and in ΔP2 .

5 Conclusions

In this paper, we have proposed an imperfect information variant of the alternation-free alternating μ-calculus from [2]. The idea is very simple: af-AMCi is a modification of af-AMC with imperfect information semantics of one-step modalities 〈A〉, plus explicit modalities for reasoning about agents' knowledge. We show that the new logic allows to specify properties which cannot be expressed in ATLir nor ATLiR. Somewhat surprisingly, the converse also holds: there are properties expressible in ATLir and ATLiR which have no counterparts in af-AMCi. Thus, unlike af-AMC which strictly extends ATL in perfect information scenarios, af-AMCi and ATL variants for imperfect information seem to have different agendas. ATL allows to reason about properties that the agents know how to achieve from the current state of the system. af-AMCi formulae refer to properties that the agents will know how to achieve all along the play because they are able to recompute the right strategy at any moment.

We also point out that model checking af-AMCi specifications can be done in polynomial time for small coalitions; for larger groups of agents, the verification complexity is the same as for ATLir. So, the new logic allows to specify a new intuitive class of strategic properties, and at the same time has a tractable model checking problem - albeit in a somewhat limited scope. We consider the result significant. To our knowledge, af-AMCi is the first strategic logic of imperfect information with tractable verification for a relevant subset of formulae. Even solving 2-player extensive form games with binary payoffs is NP-complete in any reasonable sense (e.g., for surely winning). Model checking of all existing variants of ATL with imperfect information is at least ΔP2 -hard even for 1-player(!) turn-based ICGS's. The conceptual and computational aspects hopefully make af-AMCi appealing in practical contexts.

A deeper study on specification and verification issues wrt. the alternating epistemic μ-calculus is left for future research.

Acknowledgements. Wojciech Jamroga acknowledges the support of the FNR (National Research Fund) Luxembourg under project S-GAMES - C08/IS/03.