Andreas Herzig
email: herzig@irit.fr

Logics of knowledge and action: critical analysis and challenges

Keywords: Logic of action, Logic of knowledge, Common knowledge, Frame problem, Uniform strategy

We overview the most prominent logics of knowledge and action that were proposed and studied in the multiagent systems literature. We classify them according to these two dimensions, knowledge and action, and moreover introduce a distinction between individual knowledge and group knowledge, and between a nonstrategic an a strategic interpretation of action operators. For each of the logics in our classification we highlight problematic properties. They indicate weaknesses in the design of these logics and call into question their suitability to represent knowledge and reason about it. This leads to a list of research challenges.

Introduction

A central issue in the study of multiagent systems (MAS) is the formal analysis of its relevant concepts as well as their interplay. Agents are typically analysed in terms of the concepts of knowledge, belief, desire, goal, and intention; their interaction is typically analysed in terms of the concepts of action, event, and time. Following a well-established tradition in philosophical logic and in the artificial intelligence subfield of knowledge representation, many researchers have directed their attention to formal logics in order to account for these concepts and design appropriate logical languages enabling formal reasoning.

In this paper we focus on the logics of two concepts playing a fundamental role in MAS: knowledge and action. They are of utmost importance in any area of research whose aim is to model intelligent agents, be they human or artificial. Typical situations to be modelled are when agents with imperfect knowledge perform actions in order to achieve goals. Often the resulting models involve not only individual knowledge and individual actions, but also group knowledge and joint actions. For example, the joint actions of speakers and hearers in a dialogue build the common ground, which has been analysed in the literature as a kind of group knowledge.

The main logics of knowledge and action that were proposed in the philosophical and computer science literature are modal logics: extensions of classical propositional logic by modal operators. The latter enable us to talk in a natural way about what an agent knows and what the effects of his actions are. For example, the modal operator of knowledge is written K i , where i is an agent name and where the formula K i ϕ reads "i knows that ϕ"; and the modal operator of ability is written i , where the formula i ϕ reads "i can achieve ϕ". These two kinds of operators combine in a natural way: for example, the formula i K j ϕ expresses that i can achieve that j knows that ϕ, and the formula K i ¬ j ϕ expresses that i knows that j cannot achieve ϕ. Furthermore, we distinguish two different readings of action operators. In a nonstrategic reading we say that i can achieve ϕ if the other agents do not act; in a strategic reading we say that i can achieve ϕ whatever the other agents do. We reserve the traditional 'diamond' modal operator i for the former reading and use [i] for the latter, combining a modal diamond and a modal box in a way that renders its 'exists/for all' quantification. The notation generalises from individual agents to groups.

The first contribution of the present paper is a classification of the main logics of action and knowledge along the knowledge dimension and the action dimension. In the knowledge dimension we distinguish logics that do not account for knowledge at all, logics that only account for individual knowledge, and logics that account for group knowledge; and in the action dimension we distinguish logics that do not account for actions at all, logics that only have nonstrategic action operators, and logics that have strategic action operators. This makes up a 3×3 grid. Its simplest element is classical propositional logic: the logic which neither accounts for knowledge nor for action. The other eight categories are extensions of classical propositional logic by particular families of modal operators.

Our second and main contribution is a critical assessment of the most prominent existing logics in each of the eight relevant categories. For all but classical propositional logic we highlight one or more problematic properties. They can be traced back either to the design of the logical language-some natural statements cannot be expressed-or to the design of the logic itself-either too many or too little theorems. The former property affects the suitability of these logics for knowledge representation while the latter affects their suitability for drawing appropriate conclusions from the knowledge once it has been represented. Some of these problems had already been identified in particular in the philosophical literature. However, they were often ignored in the MAS and artificial intelligence literature.

We present each logic syntactically: we entirely omit the semantical aspects of the logics (which are quite involved in some cases) and instead list and discuss for each logic under examination its logical principles, i.e., its axioms and inference rules. This suffices to explain the problems that we want to point out, while providing at the same time a concise and uniform presentation. It also squares well with our knowledge representation perspective. This said, we are aware that much of the work on logics for MAS is heavily semantic-driven, foremost in the temporal logic literature where there was a 'theorem proving vs. model checking' debate [START_REF] Halpern | Model checking vs. theorem proving: A manifesto[END_REF] and where model checking is the most important reasoning technique. The model checking perspective was also adopted by several authors in the epistemic logic literature [START_REF] Lomuscio | Model checking knowledge, strategies, and games in multiagent systems[END_REF][START_REF] Penczek | Verifying epistemic properties of multi-agent systems via bounded model checking[END_REF]. In the 'theorem proving vs. model checking' debate the main argument for the latter was better chances for decidability and a generally lower complexity. We would however like to separate such more mathematical concerns from our present more philosophical concerns: the conceptual analysis should precede the investigation of computational properties, and we believe that the conceptual weaknesses that we are going to highlight are important enough to justify our enterprise.

The rest of the paper is organised as follows. In Sect. 2 we introduce two kinds of modal operators of knowledge and two kinds of modal operators of action, leading to a grid of nine classes of MAS logics. In the remaining sections we basically examine one exemplary logic per class, omitting the class having neither action nor knowledge operators. For two of the classes we present two logics. We start by examining logics without knowledge operators: Propositional Dynamic Logic (PDL) and Coalition Logic of Propositional Control (CL-PC) as logics with nonstrategic action operators (Sect. 3) and Alternating-time Temporal Logic (ATL) and Seeing-To-It-That Logic (STIT) as logics with strategic action operators (Sect. 4).The following three sections examine logics with operators of individual knowledge: the basic epistemic logic S5 (Sect. 5), Public Announcement Logic (PAL) as a logic with nonstrategic action operators (Sect. 6), and Alternating-time Epistemic Temporal Logic (ATEL) as a logic with strategic action operators (Sect. 7). The last three sections are about extensions of some underlying logic with the common knowledge operator: S5 CK extends S5 (Sect. 8), PAL CK extends PAL (Sect. 9), and ATEL CK extends ATEL (Sect. 10). Based on the critiques of the preceding sections, Sect. 11 concludes by a list of research challenges.

A classification of MAS logics

We start by introducing a modal language that extends the language of classical propositional logic by modal operators of knowledge and modal operators of action. We distinguish two kinds of modal operators of knowledge and two kinds of modal operators of action.

Beyond the logical operators our language has the following non-logical symbols: propositional variables, action names, and agent names. More precisely, we suppose given -a countable set of propositional variables P = { p, q, q 1 , . . .}; -a countable set of action names A = {a, b, b 1 , . . .}; -a finite set of agent names I = {i, j, j 1 , . . .}.

Nonempty subsets of I are called groups or coalitions. 1 For a given coalition J , the elements of its complement J = I \ J are called the opponents of J . Throughout the paper we use the term 'group' in general, while we use 'coalition' only when we reason strategically, i.e., when we take into account what the coalition's opponents might do (cf. the readings of the ability operators in Sect. 2.2).

All the logics in this paper will be presented syntactically, in terms of axiomatisations made up of axiom schemas and inference rules. All of them have a classical basis that we do not list explicitly: some axiom schemas for classical propositional logic plus the inference rule of modus ponens. A deduction of a formula ϕ from a set of formulas Γ is a finite sequence of formulas whose last element is ϕ and which is such that each element of the sequence is either an element of Γ , or an instance of an axiom schema, or is obtained from preceding elements in the sequence by an inference rule. This is called deduction with global hypotheses in modal logic. One may also define deduction with local hypotheses; the definition is a bit more complicated. When ϕ is deducible from Γ with the axiomatisation L then we write Γ ⊢ L ϕ. When Γ = {χ} is a singleton we write χ ⊢ L ϕ, and when γ is empty we write ⊢ L ϕ instead of ∅ ⊢ L ϕ. In the latter case the deduction is called a proof, and provable formulas are called theorems.

Modal operators of knowledge

The modal operators of knowledge are parametrised by either an individual agent or a set of agents. In the former case of individual knowledge, modal formulas take the form K i ϕ where ϕ is a formula and are read "agent i knows that ϕ". In the latter case we distinguish several kinds of group knowledge: shared, common and distributed.

A formula ϕ is shared knowledge in the group of agents J , written EK J ϕ, if each agent in J knows that ϕ. EK J ϕ is therefore identical to the conjunction of individual knowledge:

EK J ϕ ↔ i∈J K i ϕ.
In most presentations EK J ϕ is actually defined as an abbreviation of i∈J K i ϕ. The concept can therefore be added without any technical difficulties to a logic of individual knowledge, and we do not present it in more detail here.

A formula ϕ is common knowledge in J , written CK J ϕ, if it is shared knowledge that ϕ, it is shared knowledge that it is shared knowledge that ϕ, and so on. Intuitively, CK J ϕ is therefore equivalent to an infinite conjunction:

CK J ϕ ↔ EK J ϕ ∧ EK J EK J ϕ ∧ EK J EK J EK J ϕ ∧ • • • .
Such an infinite conjunction is however not a well-formed formula: differently from the shared knowledge operator, the common knowledge operator cannot be defined from the modal operators of individual knowledge by means of an abbreviation. The way out is to add the modal operators CK J to the language and to give them the status of full-fledged logical connectives.

A formula ϕ is distributed knowledge in group J if ϕ follows from the combined knowledge of the agents in J . It is somewhat difficult to grasp the concept syntactically beyond that informal definition. We here do so only in an approximate manner and view distributed knowledge as 'hypothetical common knowledge': ϕ is distributed knowledge in the group of agents J , written DK J ϕ, if it is the case that when each agent communicates all his individual knowledge to all the other agents in J then ϕ becomes common knowledge in J . We do not go into the details for two reasons: first, the standard way of presentating distributed knowledge is semantical (in terms of the intersection of the accessibility relations of the group members) and cannot be characterised axiomatically (because intersection of accessibility relations is not modally definable); second, its semantics has some known conceptual problems: there are Kripke models where formally there is distributed knowledge that ϕ, while intuitively this is not the case [START_REF] Meyer | Epistemic logic for AI and computer science[END_REF][START_REF] Roelofsen | Distributed knowledge[END_REF]. Moreover, distributed knowledge was not studied to the same extent as common knowledge. We are going to discuss it briefly in two places: in Sect. 9.3 we explain the shortcomings of our definition of distributed knowledge as hypothetical common knowledge when examining the extension of Public Announcement Logic (PAL) with group knowledge, and in Sect. 10 we discuss the role of distributed knowledge when investigating uniform strategies in logics with group knowledge.

Common knowledge implies shared knowledge, shared knowledge implies individual knowledge, individual knowledge implies distributed knowledge, and distributed knowledge implies truth; in formulas, we have

CK J ϕ → EK J ϕ, EK J ϕ → K i ϕ if i ∈ J , K i ϕ → DK J ϕ
Individual K i ϕ "Agent i knows that ϕ" Group EK J ϕ "It is shared knowledge in J that ϕ",
"Every agent in J knows that ϕ"

CK J ϕ "It is common knowledge in J that ϕ" DK J ϕ "It is distributed knowledge in J that ϕ"
if i ∈ J , and DK J ϕ → ϕ. In the case of singleton groups, all three concepts of group knowledge coincide with individual knowledge: the formulas CK {i} ϕ, EK {i} ϕ, K i ϕ, and DK {i} ϕ are all equivalent.

The different modal operators of knowledge and their readings are listed in Table 1.

Modal operators of action and ability

The modal operators of action relate an agent or group of agents to a formula that is viewed as the outcome of the agent's action. Most of the MAS logics deal with potential action, as opposed to actual action: they talk about the ability of an agent or a group of agents to achieve some outcome, and not about what they actually do. We are therefore mainly going to deal with modal operators of ability.

Modal operators of ability can be interpreted in two ways. In the nonstrategic interpretation it is supposed that no other action is performed: the outcome is achieved ceteris paribus. In the strategic interpretation the outcome is achieved whatever the other agents do. (There seems to be no scholarly name for that opposite of ceteris paribus; ceteris mutandis, ceteris variantis, or ceteris agentis might be suitable.) The strategic interpretation is appropriate to reason about strategic games, where one studies whether an agent or a coalition of agents has a winning strategy.

-In the nonstrategic interpretation, modal formulas take the form J ϕ and are read "group J can achieve ϕ while the other agents don't act". -In the strategic interpretation, modal formulas take the form [J ] ψ and are read "coalition J can achieve ψ whatever the opponents do". 2In nonstrategic contexts we talk about groups, while in strategic contexts we talk about coalitions and their opponents.

Only the so-called modal logics of agency deal with actual action. We here limit ourselves to one such operator: the operator of seeing-to-it-that, abbreviated 'stit' [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF][START_REF] Horty | Agency and deontic logic[END_REF]. Agency formulas take the form Stit J ϕ and are read "J achieves ϕ whatever the opponents do". There exists another tradition studying a similar modal operator of agency that is read "i brings it about that" [START_REF] Elgesem | The modal logic of agency[END_REF][START_REF] Herzig | Action theories[END_REF][START_REF] Pörn | Action theory and social science: Some formal models[END_REF]. We do not discuss it here because the logics of these operators lack the modal operator of historical possibility: the latter will be instrumental for us in Sect. 7, where we relate stit logics to other strategic logics in order to solve the problems occurring there.

All the modal operators of action that we have introduced up to now relate agents and outcomes, but leave implicit the action the agent performs to achieve the outcome. There exist logics with names for actions in the language. Beyond such atomic actions they also allow to talk about complex actions, that may also be called plans. Complex actions are built from atomic actions by means of program operators such as sequential composition and iteration. Modal formulas take the form π ϕ and are read "there is an execution of plan π after which ϕ". In principle such so-called dynamic operators can be interpreted both in a nonstrategic and in a strategic way. The only standard logic in the literature with such dynamic operators, PDL, comes with the first interpretation. However and as we will discuss in Sect. 4, logics with strategic operators [J ] that are indexed by actions committing some agents to perform some actions were proposed recently in the literature. When the committed agents are exactly those of J then we obtain a dynamic operator with a strategic interpretation. While the standard syntax of PDL does not provide agent names, we suppose that each action name a ∈ A comes with an agent name i ∈ I identifying the author of a. This is written a i or i:a. The logical language is extended in this way in many papers in the MAS literature, for example in [START_REF] Herzig | A dynamic logic of agency I: STIT, abilities and powers[END_REF][START_REF] Hustadt | Reasoning about agents in the karo framework[END_REF][START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF].

The different modal operators of ability and action are summarised in Table 2.

The grid of MAS logics

Our classification of logics according to the knowledge and the action dimension leads to the nine classes of logics that are depicted in the 3×3 grid in Table 3. We do not mention there any logic lacking both knowledge operators and action operators: this would be good old classical propositional logic, which it is not interesting for our enterprise.

For each of the remaining eight classes we give one prominent logic. As we have motivated above, we discuss further representatives for the two classes of logics without knowledge operators: in the nonstrategic category we discuss PDL and in the strategic category we discuss STIT.

In the rest of the paper we are going to critically examine each of the ten logics in our grid.

No uncertainty, nonstrategic actions: PDL and CL-PC

We start by recalling PDL, which is a logic with names for actions, and show that it suffers from the frame problem. We then present a dialect of PDL solving the frame problem, Dynamic Logic of Propositional Assignments (DL-PA). We finally recall CL-PC, which is a logic without explicit actions, and present its embedding into DL-PA.

Propositional Dynamic Logic (PDL)

The authors of PDL [START_REF] Harel | Dynamic logic[END_REF][START_REF] Harel | Dynamic logic[END_REF] were motivated by the verification of computer programs. Later, PDL was also applied in philosophy of action [100]. Its language has modal formulas of the form π ϕ, where ϕ is a formula and π is a complex action-alias a plan or a program-, read "there exists a possible execution of π after which ϕ" or "action π possibly achieves ϕ (if the opponents do nothing)". The latter reading indicates that in PDL, the interpretation of actions is nonstrategic. The modal operator π comprehends an existential quantification; a dual operator [π] with a universal quantification is defined by the abbreviation [π]ϕ def = ¬ π ¬ϕ. It therefore has to be read "ϕ after every possible execution of π" or "π necessarily achieves ϕ (if the opponents do nothing)". The program π is either an atomic program a, a sequential composition π ; π , a nondeterministic composition π ∪ π , a finite iteration π * , or a test ϕ?, where ϕ is a formula. The standard programming instructions can then be defined as PDL programs: for example, the program ⊤? is the 'skip' action, (ϕ?; π 1 ) ∪ (¬ϕ?; π 2 ) is nothing but the conditional "if ϕ then π 1 else π 2 " and (ϕ?; π) * ; ¬ϕ? is the loop "while ϕ do π".

The star-free fragment of PDL is the set of formulas without the iteration operator * , that is also called 'Kleene star'.

As we have already said in Sect. 2.2, while the original language of PDL is not designed for multiple agents, one may nevertheless accommodate them by indexing atomic actions with agent names: we suppose that the members of the set of action names A have the form i:b where i is an agent and b is an action name. For example, the formula i 1 :b 1 ⊤ ∧ [i 2 :b 1 ]⊥ expresses that i 1 is able to perform b 1 and i 2 is not.

The axiomatisation of PDL is given in Table 4. The principles in the left column, RE( π ), N( π ), M( π ), C( π ), and Dual( π ), are common to all so-called normal modal logics [START_REF] Blackburn | Modal logic. Cambridge tracts in theoretical computer science[END_REF][START_REF] Chellas | Modal logic: An introduction[END_REF]; M( π ) and C( π ) can be replaced by the axiom K( π ):

([π]ϕ ∧ [π](ϕ→ψ)) → [π]ψ. The right column of
χ ⊢ PDL ϕ iff ⊢ PDL (i 1 :b 1 ∪ • • • ∪ i n :b n ) * χ → ϕ,
where {i 1 :b 1 , . . . , i n :b n } is the set of atomic actions occurring in ϕ.

The problem of deciding the satisfiability of a PDL formula is PSPACE complete for the star-free fragment and EXPTIME complete for the full language [START_REF] Pratt | A near-optimal method for reasoning about action[END_REF].

Reasoning about ability and the frame problem

In PDL, one can describe an atomic action i:b by means of formulas stating its preconditions and (possibly conditional) effects. These formulas respectively take the form Precond → i:b ⊤ and Cond → [i:b]Effect. A set of such formulas makes up a theory

( π ) ϕ ↔ ϕ ′ π ϕ ↔ π ϕ ′ Seq π 1 ; π 2 ϕ ↔ π 1 π 2 ϕ N( π ) ¬ π ⊥ Nondet π 1 ∪ π 2 ϕ ↔ π 1 ϕ ∨ π 2 ϕ M( π ) π (ϕ ∨ ψ) → π ϕ ∨ π ψ Test ϕ? ψ ↔ ϕ ∧ ψ C( π ) π ϕ ∨ π ψ → π (ϕ ∨ ψ) FP( π * ) π * ϕ ↔ ϕ ∨ π π * ϕ Dual( π ) [π ]ϕ ↔ ¬ π ¬ϕ LFP( π * ) π * ϕ → ϕ ∨ π * (¬ϕ ∧ π ϕ)
of actions ActionTheory. Given ActionTheory, one typically wants to check whether given the description of the initial state Init, the group of agents {i 1 , . . . , i n } is possibly able to achieve the goal Goal by means of a sequence of atomic actions i 1 :b 1 ; • • • ; i n :b n . This is the most basic multiagent version of a prediction task. More elaborate versions with synchronous or asynchronous execution of actions can be designed [START_REF] Fagin | Reasoning about knowledge[END_REF]. Formally, the above prediction task amounts to checking whether Init → i 1 :b 1 ; • • • ; i n :b n Goal can be deduced from ActionTheory, i.e., to checking whether

ActionTheory ⊢ PDL Init → i 1 :b 1 ; • • • ; i n :b n Goal.
The above formula only guarantees that the group is possibly able to achieve ϕ. If actions are nondeterministic then we often rather want to know whether the group is necessarily able to achieve ϕ. We then have to check the deducibility of the following formula:

ActionTheory ⊢ Init → i 1 :b 1 ; • • • ; i n :b n ⊤ ∧ [i 1 :b 1 ; • • • ; i n :b n ]Goal .
Let us suppose we want to formulate an action theory for a domain containing the action i:moveBlock L 1 ,L 2 of agent i moving some block from location L 1 to L 2 . Suppose the set of propositional variables P contains BlockRed. Then the action theory has to contain the two implications

BlockRed → [i:moveBlock L 1 ,L 2 ]BlockRed, ¬BlockRed → [i:moveBlock L 1 ,L 2 ]¬BlockRed
in order to guarantee that the colour of the block is not altered by moving it. Formulas of that form are called frame axioms. Intuitively, action theories should not contain such formulas; instead, they should rather be deducible from it. This however fails to be the case here: the logic PDL is too weak and suffers from the so-called frame problem [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF]. Formally and according to Reiter [START_REF] Reiter | Knowledge in action: Logical foundations for specifying and implementing dynamical systems[END_REF], an appropriate reasoning about actions formalisms should have action descriptions with size much smaller than Car d(P) × Car d(I) (assuming that P is finite). His argument appeals to the principle of inertia, which basically says that an action only modifies the truth value of very few propositional variables and leaves the others unchanged.

In contrast, the addition of frame axioms to a PDL action theory results in a set of formulas whose size is in the order of Car d(P) × Car d(I).

Reiter's solution to the frame problem

The frame problem not only plagues PDL, but virtually every logic-based framework for reasoning about a dynamic system. Interestingly, it was also investigated during the last decade in theoretical computer science, where separation logic is considered to be a solution that enables local reasoning about memory structures such as heaps or chained lists [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF]. In the artificial intelligence field of reasoning about actions, a lot of dedicated logical formalisms were developed in the eighties in order to solve the frame problem, including the Situation Calculus [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF], the Event Calculus [101], the Fluent Calculus [103], and so-called action languages such as A, B, C, C+, and most recently BC [START_REF] Gelfond | Action languages[END_REF][START_REF] Lee | Action language BC: Preliminary report[END_REF].

One of the most popular solutions to the frame problem is Reiter's [START_REF] Reiter | The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression[END_REF][START_REF] Reiter | Knowledge in action: Logical foundations for specifying and implementing dynamical systems[END_REF] in terms of what he calls successor state axioms. While Reiter's original framework was the Situation Calculus, his solution can be imported into PDL if we augment it by variables for action names, quantifiers and the equality predicate. We call the resulting logic PDL ∀ . We know of no result in the literature about the precise relationship with first-order dynamic logic [START_REF] Harel | Dynamic logic[END_REF][START_REF] Harel | Dynamic logic[END_REF] where variables do not range over atomic programs but over objects of the world (just as in first-order logic) and just note that the two logics are a priori different.

The successor state axiom for the propositional variable BlockRed can be formulated in

PDL ∀ as ∀x [x]BlockRed ↔ x=(i:paintRed) ∨ (BlockRed ∧ x =(i:paintBlue)) ,
where in order to simplify we suppose that i is the only agent who is able to paint and that the only available colours are red and blue. The general form of a successor state axiom for a propositional variable p is

∀x [x] p ↔ γ p (x) ,
where x is a variable ranging over the set of actions and γ p (x) is a boolean formula. It determines the truth value of p after action x given the truth value of γ p (x) before x. This presupposes complete knowledge about the pre-and postconditions of each action a. In other words, Reiter's solution does not work when there are integrity constraints, such as that a block cannot be both red and blue and that a block must have a colour. Taking such constraints into account would pose the ramification problem.

Reiter's basic action theories have one successor state axiom per propositional variable in P. This solves the frame problem: the cardinality of a basic action theory is linear in that of P, and if we suppose with Reiter that the length of each successor state axiom is bounded then we obtain an action theory whose size is also linear in that of P.

While the basic version of Reiter's solution is for deterministic actions only, nondeterminism can be modelled by means of PDL's operator of nondeterministic composition.

To sum it up, the adoption of Reiter's solution seems to require quantification over action names, which is not available in PDL. However, as we will show in the sequel, Reiter's solution can be captured in a simple variant of PDL that stays in the propositional realm.

DL-PA: a variant of PDL solving the frame problem

It was shown in [114] that Reiter's basic action theories can be captured in a dialect of PDL. Its extension by the PDL program operators, called DL-PA, was further studied in [START_REF] Balbiani | Dynamic logic of propositional assignments: A wellbehaved variant of PDL[END_REF][START_REF] Herzig | A dynamic logic of normative systems[END_REF]. We first describe that logic and then the embedding.

The language of DL-PA is just as that of PDL, except that atomic actions are not just abstract names: they do something concrete, namely to assign formulas ϕ to propositional variables p. Such assignments are written p:=ϕ. The original language only contains assignments of ⊤ and ⊥; however, the more general assignment p:=ϕ can be considered to be an abbreviation of (ϕ?; p:=⊤)∪(¬ϕ?; p:=⊥). For example, BlockAt L 1 :=⊥ makes BlockAt L 1 false. We here only present an axiomatisation of star-free DL-PA and refer the reader to the above papers for the full logic. The four axiom schemas that have to be added to those of PDL are the following:

p:=ϕ ψ ↔ [ p:=ϕ]ψ p:=ϕ p ↔ ϕ q ↔ p:=ϕ q for q = p
The first says that assignments are serial and deterministic. The second says that p is true after the assignment of ϕ to p if and only if ϕ was true before. The third says that assignments to p do not modify other variables.

Reasoning in DL-PA has several advantages over PDL: the logic is compact and has the interpolation property; model checking has the same complexity as satisfiability checking; the Kleene star is eliminable (from which it follows that every DL-PA formula is reducible to a boolean formula). Complexity of satisfiability is PSPACE complete for its star-free fragment [START_REF] Herzig | A dynamic logic of normative systems[END_REF].

The fact that the execution of an assignment p:=ϕ leaves unchanged the truth values of all those q that are different from p leads to a solution to the frame problem. For example, the action i:moveBlock L 1 ,L 2 can be captured by the DL-PA program

i:moveBlock L 1 ,L 2 = (Rep i:moveBlock L 1 ,L 2 ?; Free?; BlockAt L 1 :=⊥; BlockAt L 2 :=⊤),
where we suppose that the propositional variables Rep i:moveBlock L 1 ,L 2 and Free are true when the action moveBlock L 1 ,L 2 is in agent i's repertoire and when the block is free, respectively. For that action, the formulas

BlockRed → [i:moveBlock L 1 ,L 2 ]BlockRed, ¬BlockRed → [i:moveBlock L 1 ,L 2 ]¬BlockRed are both DL-PA theorems.
Let us make this precise. A successor state axiom ∀x [x] p ↔ γ p (x) is explicit if for every a that does not occur in γ p (x), γ p (a) ↔ p is a theorem of classical propositional logic. For such actions [a] p ↔ p is therefore a theorem, which means that an action that does not occur in γ p (x) cannot modify p. Special cases are Reiter's original definition of successor state axioms [START_REF] Reiter | The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression[END_REF] and local effect successor state axioms [118]. The successor state axiom for BlockRed in Sect. 3.3 is clearly explicit.

The theorem below basically says that for explicit basic action theories, action a's effects according to Reiter are exactly the effects of the DL-PA assignment program

π a = q a 1 :=γ q a 1 (a); • • • ; q a n :=γ q a n (a)
, where q a 1 , . . . , q a n are all variables whose successor state axiom mentions a. It is formulated for the extension PDL ∀ of PDL by action variables, quantification and equality within which we have presented Reiter's solution in Sect. [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF]

.3 and follows from Theorem 18 of [114]. 3

Theorem 1 Let ActionTheory be a set of explicit successor state axioms, one per propositional variable p. Let ϕ be some PDL formula. For each atomic program a, let {q a 1 , . . . , q a n } be the set of propositional variables q a k such that a occurs in the successor state axiom for q a k and such that q a k occurs in ϕ. Let ϕ ′ result from replacing each abstract atomic action a in ϕ by the complex assignment program π a = q a 1 :=γ q a 1 (a); • • • ; q a n :=γ q a n (a) . Then

ActionTheory ⊢ PDL ∀ ϕ if and only if ⊢ DL-PA ϕ ′ .
The length of ϕ ′ is quadratic in the length of ϕ, and the embedding of Reiter's solution to the frame problem is therefore polynomial [114, Theorem 27].

One might argue that the above result is not very impressive: after all, frame axioms can also be encoded in PDL by systematically augmenting action theories with a polynomial number of frame axioms. We have seen in the end of Sect. 3.2 that this however violates Reiter's criterion for a solution to the frame problem because the cardinality of the action theory is in the order of Car d(P)×Car d(I). In contrast, the encoding into DL-PA is satisfactory because it is based on Car d(A) action descriptions π a , one per action a ∈ A. Differently from PDL and the Situation Calculus, these action descriptions appear directly in the formula, i.e., there are no action names that are axiomatised separately in an action theory.

We view DL-PA as a sort of Assembler language for reasoning about change. Its applicability to update and revision operations, planning tasks, argumentation theory and answer-set programming has been demonstrated recently [START_REF] Doutre | A dynamic logic framework for abstract argumentation[END_REF][START_REF] Del Cerro | Combining equilibrium logic and dynamic logic. Logic programming and nonmonotonic reasoning[END_REF][START_REF] Herzig | Belief change operations: A short history of nearly everything, told in dynamic logic of propositional assignments[END_REF][START_REF] Herzig | On the revision of planning tasks[END_REF]. In the rest of the section we show that it captures a logic of ability.

Coalition Logic of Propositional Control (CL-PC) and its embedding into DL-PA

Coalition Logic of Propositional Control (CL-PC) was introduced in [110,112]. It is a MAS logic with nonstrategic actions that does not account for uncertainty. Just as in boolean games [START_REF] Bonzon | Boolean games revisited[END_REF][START_REF] Harrenstein | Boolean games[END_REF], the idea is that each propositional variable is controlled by some agent. When i controls p then i can modify the truth value of p at will. An action of i is therefore identified with the change of some of i's variables. It is supposed that control is not only exclusiveeach variable is controlled by at most one agent-, but also exhaustive -each variable is controlled by at least one agent.

The language of CL-PC relates agents to outcomes. It has formulas of the form J ϕ, read "group J can achieve ϕ by modifying its variables while the opponents don't act". The dual [J ]ϕ may be read "group J cannot prevent ϕ". The fact that i controls p can then be expressed by the CL-PC formula i p ∧ i ¬ p.

We do not give the entire axiomatics of CL-PC here and refer the reader to [110]. Instead, the principles of the logic will become clear through the embedding into DL-PA that we state as Theorem 2. But let us first discuss two CL-PC theorems in order to limber up:

i p ∧ i ¬ p → [i] i p ∧ i ¬ p , i p ∧ i q → i ( p∧q).
The first theorem says that an agent's action repertoire is not changed by the performance of actions. The second theorem comes from the fact that control is exercised over atomic formulas and not over complex formulas. Note that these are theorems and not theorem schemas; for example, the replacement of q by ¬ p in the last formula results in a nontheorem.

The focus of CL-PC is reasoning about nonstrategic (ceteris paribus) ability: given a set of CL-PC formulas AbilityTheory describing the abilities of the different agents by means of formulas of the form i p ∧ i ¬ p, one may check whether AbilityTheory ⊢ CL-PC Init → {i 1 , . . . , i n } Goal holds, where Init describes some initial situation and Goal some goal. As the agents' repertoires are not changed by the performance of actions, this is the same as

⊢ CL-PC (AbilityTheory ∧ Init) → {i 1 , . . . , i n } Goal.
Let P ϕ be the set of propositional variables occurring in ϕ. For every agent i ∈ I and variable p ∈ P ϕ , let Ctrl i, p be a fresh propositional variable (not occurring in ϕ); the intended meaning of Ctrl i, p is that i controls p. Then the formulas

Excl ϕ = p∈P ϕ i, j∈I,i = j ¬(Ctrl i, p ∧ Ctrl j, p ), Exh ϕ = p∈P ϕ i∈I Ctrl i, p
describe exclusivity and exhaustivity of the control over P ϕ .

Given a set of agents J and a propositional variable p, we define the following program:

vary J, p = ⊤? ∪ i∈J Ctrl i, p 1 ?; p 1 :=¬ p 1 .
It either does nothing or flips the truth value of p if p is under the control of one of J 's members. For example:

vary {i}, p p = ⊤? ∪ (Ctrl i, p ?; p:=¬ p) p ↔ ⊤? p ∨ Ctrl i, p ? p:=¬ p p ↔ p ∨ (Ctrl i, p ∧ ¬ p) ↔ p ∨ Ctrl i, p .
Therefore [vary {i}, p ] p ↔ p ∧ ¬Ctrl i, p . Then for a finite set of propositional variables P = { p 1 , . . . , p n } ⊆ P, we define vary J,P = vary J, p 1 ; • • • ; vary J, p n which nondeterministically changes the truth value of some of the variables of P that are under J 's control. The theorem below is a consequence of Theorems 4 and 5 of [START_REF] Herzig | A dynamic logic of normative systems[END_REF].

Theorem 2 Let ϕ be a CL-PC formula and let ϕ ′ be the DL-PA formula resulting from replacing each subformula J ψ of ϕ by vary J,P ψ ψ. Then

⊢ CL-PC ϕ if and only if ⊢ DL-PA (Exh ϕ ∧ Excl ϕ ) → ϕ ′ .
Note that the length of ϕ ′ is polynomial in that of ϕ.

Strategic reasoning in CL-PC

It was argued in [110] that in CL-PC one can also reason about strategic ability: as pointed out there, the CL-PC formula J [J ]ϕ expresses that J can achieve ϕ next whatever J 's opponents do. It is claimed that this captures at least the spirit of the formula [J ] Xϕ of Pauly's Coalition Logic CL. Indeed, if we take a CL theorem and replace its strategic operators [J ] X by J [J ] then the resulting formula is a CL-PC theorem [110, Theorem 4.1].

In the rest of the section we have a look at the other direction.

Consider the following equivalence:

ϕ 0 = J [J ]( p∨q) ↔ J [J ] p ∨ J [J ]q
It basically says that if J can achieve p∨q whatever its opponents do then either J controls p or J controls q. We are going to establish that it is a theorem of CL-PC. The difficult part is to prove that

ψ 0 = [J ]( p∨q) ↔ [J ] p ∨ [J ]
q is a theorem of CL-PC; the rest follows by principles of normal modal logics. We prove that

ψ ′ 0 = [vary J ,{ p,q} ]( p∨q) ↔ [vary J ,{ p} ] p ∨ [vary J ,{q} ]q
is a theorem of DL-PA, from which it follows by Theorem 2 that ψ 0 is a theorem of CL-PC.

The following equivalences are all theorems, where we write Ctrl J, p instead of i∈J Ctrl i, p :

[vary J ,{ p} ] p∨[vary J ,{q} ]q ↔ p∧¬Ctrl J , p ∨ q∧¬Ctrl J ,q ↔ p ∧ (¬Ctrl J , p ∨¬ p) ∨ q ∧ (¬Ctrl J ,q ∨¬q) ↔ ( p∨q) ∧ ¬Ctrl J ,q ∨ p∨¬q ∧ ¬Ctrl J , p ∨¬ p∨q ∧ ¬Ctrl J , p ∨¬Ctrl J ,q ∨¬ p∨¬q ↔ [⊤?][⊤?]( p∨q) ∧ [Ctrl J ,q ?]( p∨¬q) ∧ [Ctrl J , p ?](¬ p∨q) ∧ [Ctrl J , p ?][Ctrl J ,q ?](¬ p∨¬q) ↔ [⊤? ∪ Ctrl J , p ?; p:=¬ p ][⊤? ∪ Ctrl J ,q ?; q:=¬q ] ( p∨q) = [vary J ,{ p,q} ]( p∨q) So ψ ′
0 is a theorem of DL-PA. Therefore ψ 0 is a theorem of CL-PC, and so is ϕ 0 . Let us now reformulate ϕ 0 with the modal operator of CL: we get

[J ] X( p∨q) ↔ [J ] X p ∨ [J ] Xq.
This however fails to be a theorem of CL, as we will see in the next section (Sect. 4.1). We thereby complete Theorem 4.1 of [110]: the above ϕ 0 exemplifies that the other way round, there are unprovable CL formulas whose CL-PC counterpart is a theorem.

In the next section we are going to have a closer look at the logic of strategic ability ATL, of which CL is a fragment.

No uncertainty, strategic actions: ATL and STIT

In a strategic interpretation, the sentence "coalition J is able to achieve ϕ" is understood as "J is able to achieve ϕ whatever J 's opponents do". In the present section we discuss one of the main logics with a strategic interpretation of action modalities: Alternating-time Temporal Logic (ATL). We also briefly discuss Belnap's Seeing-To-It-That Logic (STIT), which is not only about what an agent can do, but also about what an agent does.

Alternating-time Temporal Logic (ATL)

Alternating-time Temporal Logic (ATL) was introduced as a logic for distributed systems [START_REF] Alur | Alternating-time temporal logic[END_REF]. Just as those of CL-PC, the modal operators of ATL relate actions to outcomes. They combine an action modality with three temporal modalities: the formula [J ] Xϕ reads "the agents in J have a strategy such that whatever the opponents do, next ϕ"; [J ] Gϕ reads "the agents in J have a strategy such that whatever the opponents do, henceforth ϕ"; and [J ] ϕUψ reads "the agents in J have a strategy such that whatever the opponents do, ϕ until ψ". These are fused modal operators: the strategy quantifier [J ] is followed by one of the temporal operators X, G, or U. The latter stem from Linear-time Temporal Logic (LTL). Similarly

Table 5 Axiomatisation of ATL RE( [J] ) ϕ ↔ ϕ ′ [J ] Xϕ → [J ] Xϕ ′ M( [J] ) [J ] X(ϕ ∧ ψ) → [J ] Xϕ ∧ [J ] Xϕ N( [J] ) [J ] X⊤ D( [J] ) ¬ [J ] X⊥ Alt( [I] ) ¬ [∅] X¬ϕ → [I] Xϕ S( [J] ) [J 1 ] Xϕ 1 ∧ [J 2 ] Xϕ 2 → [J 1 ∪ J 2 ] X(ϕ 1 ∧ϕ 2 ) if J 1 ∩ J 2 = ∅ FP(G) [J ] Gϕ ↔ ϕ ∧ [J ] X [J ] Gϕ GFP(G) [∅] G θ → (ϕ ∧ [J ] Xθ ) → [∅] G θ → [J ] Gϕ FP(U) [J ] ψUϕ ↔ ϕ ∨ ψ ∧ [J ] X [J ] ψUϕ LFP(U) [∅] G (ϕ ∨ (ψ ∧ [J ] Xθ )) → θ → [∅] G( [J ] ψUϕ → θ )
to LTL, the formula [J ] Fϕ can be introduced as an abbreviation of [J ] ⊤Uϕ. It therefore reads "the agents in J have a strategy such that whatever the other agents do, eventually ϕ". Table 5 contains the axiomatisation of ATL [START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF]. 4 The modal operators of ATL are not normal: for example, one cannot prove

( [J ] Xϕ ∨ [J ] Xψ) → [J ] X(ϕ ∨ ψ), which is the conjunction axiom schema C (cf. Sect. 3.1)
. ATL is a so-called monotonic modal logic [START_REF] Chellas | Modal logic: An introduction[END_REF]: the monotony schema M holds for [J ] X (that has the form of PDL's schema C, cf. Table 4). The failure of the C schema is due to the fact that [J ] X contains an existential quantification followed by a universal quantification. The superadditivity schema S( [J] ) is central. It says that the abilities of disjoint coalitions J 1 and J 2 can be combined: if J 1 is able to achieve ϕ 1 and J 2 is able to achieve ϕ 2 then J 1 and J 2 together are able to achieve ϕ 1 ∧ϕ 2 . Just as PDL, ATL has a deduction theorem:

χ ⊢ ATL ϕ iff ⊢ ATL [I] Gχ → ϕ.
To decide the satisfiability of an ATL formula is an EXPTIME complete problem [120].

The language of Coalition Logic (CL) [START_REF] Pauly | A modal logic for coalitional power in games[END_REF] is the fragment of the language of ATL without G and U. It was proved in [START_REF] Goranko | Coalition games and alternating temporal logics[END_REF] that ATL is a conservative extension of CL. To decide the satisfiability of a CL formula is a PSPACE complete problem.

As we have already mentioned in Sect. 3.6, the nonstrategic CL-PC formula J [J ]ϕ of CL-PC is similar in spirit to the strategic formula [J ] Xϕ. However, they do not have exactly the same meaning. Consider the CL equivalence χ 0 = [J ] X( p∨q) ↔ ( [J ] X p ∨ [J ] Xq). We have seen in Sect. 3.6 that its CL-PC counterpart ϕ 0 is a theorem. However, if p and q are different then the left-to-right direction is neither provable in CL nor in ATL. To see this, suppose

[J ] X( p∨q) ↔ ( [J ] X p ∨ [J ] Xq) was provable in CL. Then [∅] X( p∨¬ p) ↔ ( [∅] X p ∨ [∅]
X¬ p) would be provable for any variable p by the rule of uniform substitution, which is derivable in CL. By Axiom N( [J] ) and Rule RE( [J] ) its left hand side [∅] X( p∨¬ p) is a theorem and therefore [∅] X p ∨ [∅] X¬ p would be provable for any p: the empty coalition would be able to achieve either p or ¬ p, for every p. Worse, by the 4 Actually we give an equivalent axiomatisation that better matches the other axiomatisations in this paper: our RE( monotony axiom M( [J] ) we would obtain the theorem

J ⊆I [J ] X p ∨ J ⊆I [J ]
X¬ p : all coalitions would have exactly the same power. This would make CL an uninteresting logic of strategic ability. We conclude that While we agree with van der Hoek and Wooldridge that CL-PC is an interesting logic that captures the spirit of CL, the formulas ϕ 0 and χ 0 highlight a mismatch between the two logics that can be traced back to the assumption underlying CL-PC that the agents' actions are modifications of the truth values of propositional variables. We note that ϕ 0 is not a schema, i.e., not every instance of it is a theorem. This poses the question whether CL-PC and CL differ by the status of some schema. We conjecture that no such schema exists.

The language of the logic ATL * is more liberal than that of ATL: fused modal operators such as [J ] X are decomposed into the strategy quantifier [J ] and the temporal operator X. The strategy quantifier can therefore be followed by arbitrary so-called path formulas, such as in

[{i}] ( p ∧ X p) or [{i}] G( p ∧ ¬G¬ p).
To decide the satisfiability of an ATL * formula is a 2EXPTIME complete problem [START_REF] Schewe | ATL* satisfiability is 2EXPTIME-complete[END_REF]. The language of the logic of 'seeing-to-it-that' (STIT) is even more liberal: the strategy quantifier [J ] is decomposed into an existential quantification over historic possibilities that is followed by a universal quantification over the outcomes of J 's choices. We will introduce STIT in Sect. 4.3.

Reasoning about strategies in ATL: commitments and irrevocable strategies

One can describe an agent's action repertoire (and therefore his abilities) in ATL by stating the conditioned effects of each of the agent's actions. Such formulas take the form Cond → [{i}] X Effect. This supposes that actions take a single time step and are performed by a single agent. (More general temporal postconditions and statements of joint ability are however possible, too.) A set of such formulas makes up a theory of ability AbilityTheory. Given AbilityTheory, one can typically check whether given some description of the initial state Init, a coalition of agents {i 1 , . . . , i n } is able to achieve some goal Goal in the future, whatever the opponents do. Formally, we check whether

AbilityTheory ⊢ ATL Init → [{i 1 , . . . , i n }] FGoal is the case.
While the modal operators of ATL provide an elegant and compact tool to talk about what coalitions are able to achieve against their opponents by means of strategies, strategies remain "unsung heroes" [108]: there are no names for strategies in the language and one cannot really 'grasp' them. Many authors felt that this is not satisfactory and extended ATL. Strategy Logic (SL) [START_REF] Chareton | Towards an updatable strategy logic[END_REF][START_REF] Mogavero | Reasoning about strategies[END_REF] has strategy variables and quantification over strategies; it is undecidable. The strategy quantifier of ATL with explicit strategies [121,123] is indexed by strategy names σ committing some of the agents to follow some particular strategy. For example, the formula [{Ann}] Bob:σ GMarried says that if Bob is committed to follow the strategy σ of staying faithful then Ann has a strategy ensuring that both stay married forever. Commitment to a strategy was later replaced by commitment to an action in ATL with Explicit Actions ATLEA [START_REF] Herzig | Alternating-time temporal logic with explicit actions[END_REF]. Both ATL with explicit strategies and ATLEA have the same complexity as ATL. The aim of this line of work is to index the ATL strategy quantifier with complex PDL programs. It should in particular provide a dynamic operator with a strategic interpretation; such an operator is missing up to now. The logic ATL with intentions, ATLI, of [START_REF] Jamroga | Intentions and strategies in game-like scenarios[END_REF] has a modal operator of commitment to a strategy as a first-class citizen: (str i σ i ) ϕ reads "if i intends to play according to strategy σ i then ϕ is true". This is further refined in [START_REF] Bulling | Reasoning about temporal properties of rational play[END_REF] into a logic ATL with preferences, ATLP, where one can express that agents play some equilibrium.

Introducing commitments into ATL is a way of solving the problem of reasoning with uniform strategies which plagues the epistemic extension of ATL, ATEL. We will discuss this in Sect. [START_REF] Aucher | Internal models and private multi-agent belief revision[END_REF].

Commitments can also be related to the problem of revocability of ATL strategies. Indeed, in ATL an agent i may adopt some strategy and cancel ('revoke') it at a later stage. In other words, i is never really committed to any strategy. This can be illustrated by the example of Ann and Bob who have in their repertoire the joint action of divorcing, as expressed by the ATL formula [{Ann, Bob}] X¬Married. Their repertoire also contains the action of staying married (that should perhaps better be called a non-action): Married → [{Ann, Bob}] XMarried. When AbilityTheory contains these two formulas then we have

AbilityTheory ⊢ ATL Married → [{Ann, Bob}] G Married ∧ [{Ann, Bob}] X¬Married .
So according to ATL, once Ann and Bob are married they have a strategy that (1) makes them stay married forever, and (2) allows them to abandon that strategy and to divorce at any time point. In other words, when we look at the outcome of Ann and Bob's strategy to stay together forever then we never exclude that they deviate from that strategy. Several authors felt that this is an undesirable property. Beyond the above logics with names for strategies there are two approaches that avoid the introduction of names for strategies: ATL with irrevocable strategies [1] and ATL with strategy contexts [START_REF] Brihaye | ATL with strategy contexts and bounded memory[END_REF]. The latter makes the adoption and canceling of strategies explicit. Its satisfiability problem was proved to be undecidable in [104]. The central device in the logical language are formulas of the form Stit J ϕ, read "by their current choices the agents in J guarantee that ϕ is true, whatever the other agents do". There is also an operator of historical possibility ♦ϕ, read "it is historically possible that ϕ". Its dual is defined as ϕ def = ¬♦¬ϕ and is read "ϕ is historically true" or "ϕ is settled true". The language finally has the linear-time temporal operators F ('eventually') and G ('henceforth'). Several more recent publications also include the temporal 'next' operator X [START_REF] Broersen | Embedding alternating-time temporal logic in strategic STIT logic of agency[END_REF].

The operator of historical possibility can be used to quantify over the agents' choices: the formula ♦Stit J ϕ says that J is able to achieve ϕ whatever the other agents do. So this construction resembles the ATL path quantifier [J ] , and it is not very surprising that Coalition Logic CL becomes a fragment of Chellas STIT if we translate [J ] Xϕ into ♦Stit J Xϕ [START_REF] Broersen | Embedding alternating-time temporal logic in strategic STIT logic of agency[END_REF]. An embedding of the entire language of ATL into Horty's strategic variant of STIT can be found in the same paper. It has to be noted that the operator of historic possibility is actually redundant if one admits empty coalitions: ϕ can then be viewed as an abbreviation of Stit ∅ ϕ. So ϕ is historically necessary if the empty coalition sees to it that ϕ.

The agency operators Stit J are normal modal box operators satisfying the principles of S5. The operator of historic possibility is a normal modal diamond operator also satisfying the principles of S5. Historic necessity of ϕ implies that every coalition sees to it that ϕ: the formula ϕ → Stit J ϕ is a theorem of Chellas STIT. Just as in ATL, agents and disjoint coalitions of agents are supposed to be independent. This is axiomatised for individuals by a family of axiom schemas of independence of agents [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF]Chapter 17] that resembles ATL's superadditivity:

AIA n (♦, Stit i )(♦Stit i 1 ϕ 1 ∧ • • • ∧ ♦Stit i n ϕ n ) → ♦(Stit i 1 ϕ 1 ∧ • • • ∧ Stit i n ϕ n )
A somewhat surprising consequence of this axiom is the theorem Stit i Stit j ϕ → ϕ, for i = j, in words: i can make j see to it that ϕ only if ϕ is settled true. It even turns out that a generalisation of that implication can replace the above axiom of independence of agents [START_REF] Balbiani | Alternative axiomatics and complexity of deliberative STIT theories[END_REF].

In STIT one can reason about responsibility and causality: one may check whether the coalition J is responsible for some state of affairs Fact in context Cond by checking whether the formula Cond → Stit J Fact is a STIT theorem. When this is the case then it is also said that J is agentive for Fact under the circumstances Cond.

Several authors have argued that a better account of agency is provided by the so-called deliberative stit operator that can be defined from Chellas's stit operator by means of the following abbreviation:

DStit J ϕ def = Stit J ϕ ∧ ♦¬ϕ.
Their argument is that Stit J ⊤ is a theorem of Chellas STIT: every group is agentive for a tautology. This is not the case for the deliberative stit operator: on the contrary, ¬(Stit J ⊤ ∧ ♦¬⊤) is a theorem of Chellas STIT, i.e., no group can be agentive for a tautology.

There is a price to pay for generality: satisfiability of STIT formulas is undecidable already for the language without temporal operators [START_REF] Herzig | Properties of logics of individual and group agency[END_REF]. It is decidable if coalitions are restricted to individuals, and deciding satisfiability is NEXPTIME complete [START_REF] Balbiani | Alternative axiomatics and complexity of deliberative STIT theories[END_REF].

Individual knowledge, no actions: S5

We now turn to something completely different: the logic of individual knowledge. We briefly recall the logic that is generally considered to be the standard logic of knowledge, viz. the modal logic S5, and show that it is too strong.

S5 as an epistemic logic

The logic of individual knowledge has modal operators K i , one per agent i in I. The formula K i ϕ reads "agent i knows that ϕ". Sometimes a dual modal operator Ki is used: Ki ϕ is equivalent to ¬K i ¬ϕ and reads "ϕ is consistent with i's knowledge".

Starting with Moore [START_REF] Moore | A formal theory of knowledge and action[END_REF] and Fagin et al. [START_REF] Fagin | Reasoning about knowledge[END_REF], most of the publications in computer science adopt the modal logic S5 as the logic of knowledge. We give its axiomatisation in Table 6.

As we have already mentioned in Sect. 3.1, the axiom schemas M(K i ) and C(K i ) can be replaced by the K(K i )-axiom K i ϕ ∧ K i (ϕ→ψ) → K i ψ. Each of the principles RE(K i ), N(K i ), and K(K i ) corresponds to an aspect of the omniscience problem: RE(K i ) says that an agent's knowledge is closed under logical equivalence; N(K i ) says that the agents know the tautologies; K(K i ) says that an agent's knowledge is closed under modus ponens. Axiom T(K i ) says that knowledge implies truth and distinguishes knowledge from belief. Axiom 4(K i ) is the axiom of positive introspection and 5(K i ) is the axiom of negative introspection.

(K i ) ϕ ↔ ϕ ′ K i ϕ ↔ K i ϕ ′ N(K i ) K i ⊤ M(K i ) K i (ϕ ∧ ψ) → K i ϕ ∧ K i ψ C(K i ) K i ϕ ∧ K i ψ → K i (ϕ ∧ ψ) T(K i ) K i ϕ → ϕ 4(K i ) K i ϕ → K i K i ϕ 5(K i ) ¬K i ϕ → K i ¬K i ϕ
Up to today, S5 is considered to be 'the' logic of knowledge in theoretical computer science, artificial intelligence, and dynamic epistemic logics. However, in the formal epistemology literature one can find strong arguments that S5's negative introspection axiom makes it too strong a logic of knowledge. We go into the details in the next section.

Negative introspection is undesirable!

Among others, Lenzen and Voorbraak have provided formal arguments that Axiom 5(K i ) of negative introspection is not a desirable property of a knowledge operator [START_REF] Gochet | Epistemic logic[END_REF][START_REF] Lenzen | Recent work in epistemic logic[END_REF][START_REF] Lenzen | On the semantics and pragmatics of epistemic attitudes[END_REF]119]. Perhaps the most striking argument involves its interaction with a modality of strong belief B i , called conviction by Lenzen, where the formula B i ϕ reads "agent i (strongly) believes that ϕ". The only reasoning principles that we need are K i ϕ → B i ϕ (knowledge implies belief), and ¬B i ⊥ (belief is consistent). The latter is the modal D(B i ) axiom and can be replaced by (B i ϕ ∧ B i ¬ϕ) → ⊥. Below we give a slightly modified version of the argument. Suppose ¬ p∧B i K i p is the case: i wrongly believes to know that p. Let us prove that such a hypothesis leads to inconsistency:

1. ¬ p → ¬K i p (contraposition of Axiom T(K i )) 2. ¬K i p → K i ¬K i p (Axiom 5(K i )) 3. K i ¬K i p → B i ¬K i p ('knowledge implies belief') 4. ¬ p → B i ¬K i p (from 1, 2, 3 by propositional logic) 5. (¬ p∧B i K i p) → (B i K i p ∧ B i ¬K i p)
(from 4 by propositional logic) 6.

(B i K i p ∧ B i ¬K i p) → ⊥ (Axiom D(B i )) 7. (¬ p∧B i K i p) → ⊥
(from 5, 6 by propositional logic)

The last line says that no agent can wrongly believe to know p. This is against our intuitions: one may believe to know that p, and even strongly so, but may nevertheless be wrong. Lenzen proposed that Axiom 5(K i ) should be replaced by the weaker ¬K i ¬K i ϕ → K i ¬K i ¬ϕ, which is perhaps better readable as Ki K i ϕ → K i Ki ϕ and is called Axiom .2(K i ) in the modal logic literature [START_REF] Lenzen | Recent work in epistemic logic[END_REF]. The resulting modal logic is called S4.2 and is Lenzen's 'official' logic of knowledge. Meyer and van der Hoek proposed the stronger logic S4.3 [START_REF] Meyer | Epistemic logic for AI and computer science[END_REF]. We will see in the next section that the move to S4.2 creates some new difficulties when we integrate dynamic operators.

Individual knowledge, nonstrategic actions: PAL

Starting with [START_REF] Moore | A formal theory of knowledge and action[END_REF], many authors studied the interplay of knowledge and action. We here concentrate on the interplay of knowledge and epistemic events, which only change the agents' knowledge while leaving the facts unchanged. (The term 'epistemic action' became standard in the literature, however, 'event' is more appropriate because it is supposed that the 6)

RE( ϕ! ) ψ ↔ ψ ′ ϕ! ψ ↔ ϕ! ψ ′ Dual( ϕ! ) [ϕ!]ψ ↔ ¬ ϕ! ¬ψ Red(p) ϕ! p ↔ ϕ∧ p, for p atomic Red(¬) ϕ! ¬ψ ↔ ϕ∧¬ ϕ! ψ Red(∧) ϕ! (ψ 1 ∧ψ 2 ) ↔ ϕ! ψ 1 ∧ ϕ! ψ 2 Red(K i ) ϕ! K i ψ ↔ ϕ∧K i [ϕ!]ψ
announcement is made either by the environment or by some agent that is not part of what is being modelled.) They behave just as expansion operations in Alchourrón, Gärdenfors and Makinson's AGM belief revision theory [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF]. The resulting dynamic epistemic logics were intensely studied in the last decade. We here present the simplest dynamic epistemic logic: PAL.

Public Announcement Logic (PAL)

Public Announcement Logic (PAL) extends epistemic logic by dynamic operators ϕ! of public announcement of the truth of ϕ. The formula ϕ! ψ reads "the truthful public announcement of ϕ can be made and ψ will be true afterwards". The dual [ϕ!]ψ is read "if the truthful public announcement of ϕ is made then ψ will be true afterwards". Announcements only change the agents' knowledge, but not the facts. The axiomatics of PAL is in Table 7. It follows the presentation in [START_REF] Balbiani | Some truths are best left unsaid[END_REF]. Axiom Red(p) says that announcements leave the facts unchanged. The equivalences Red(¬), Red(∧), and Red(K i ) are reduction axioms: together with Rule RE( ϕ! ) they allow to push dynamic operators inwards until they face atomic formulas. Then Red(p) allows to entirely eliminate the dynamic operators. Observe that the reduction axioms [ϕ!]K i ψ ↔ ϕ→K i [ϕ!]ψ and [ϕ!] p ↔ ψ→ p can be respectively proved from Red(K i ) and Red(¬) and from Red(p) and Red(¬).

Here is a much debated theorem of PAL: [ p∧¬K i p!]K i p. Indeed, by the reduction axioms it is successively equivalent to ( p∧¬K i p) → K i [ p∧¬K i p!] p and to ( p∧¬K i p) → K i ( p∧¬K i p)→ p , and the latter is a theorem of any normal modal logic because the right hand side of the implication is so. So after the announcement of p∧¬K i p it is true that K i p: the formula p∧¬K i p becomes false by the announcement. This so-called Moore sentence illustrates that even if what is announced is true before the announcement, it may become false by its mere announcement. Such formulas have been called unsuccessful. In contrast, non-epistemic formulas are always successful. More generally, if ϕ is a formula without any negative occurrence of epistemic operators then [ϕ!]ϕ is a theorem of PAL.

The complexity of satisfiability of PAL formulas is the same as that of the underlying epistemic logic EL [START_REF] Lutz | Complexity and succintness of public announcement logic[END_REF]. It was also shown there that if EL equals K then PAL is more succinct than EL. This was generalised by French et al. to other epistemic logics, including S5 [START_REF] French | Succinctness of epistemic languages[END_REF].

The problem of closure under updates in PAL

When it comes to choosing the epistemic logic underlying PAL, almost all authors either opt for S5 or for the basic modal logic K. This 'works' because both S5-based PAL and K-based PAL are conservative extensions of S5 and K: their theorems without the announcement operator coincide. Basically, the reason is that the axioms for the announcement operator do not interfere with the axioms of the epistemic logic. This fails to hold for other epistemic logics: PAL extensions of many logics that are intermediate between K and S5 fail to be conservative extensions. This applies in particular to the logic of belief KD45 and to Lenzen's official logic of knowledge S4.2: their extensions by the reduction axioms of PAL of Table 7 turn out to augment the theorems of the underlying epistemic logic [START_REF] Balbiani | Some truths are best left unsaid[END_REF]. Let us demonstrate this by showing that in the PAL extension of the logic of belief KD45 one can prove the knowledge axiom T(K i ).

1. ⊥ ↔ K i ⊥ (KD45) 2. ¬ϕ! ⊥ ↔ ¬ϕ! K i ⊥ (from (1) by RE( ϕ! ) 3. ¬ ¬ϕ! ⊥ (by Red(∧), Red(¬), Red(p)) 4. ¬ ¬ϕ! K i ⊥ (from (2), (3) by propositional logic) 5. ¬ ¬ϕ ∧ K i [¬ϕ!]⊥ (from (4) by Red(K i )) 6. [¬ϕ!]⊥ ↔ ϕ (by Red(∧), Red(¬), Red(p)) 7. ¬ ¬ϕ ∧ K i ϕ
(from ( 5), ( 6) by substitution of equivalents) 8. K i ϕ → ϕ (from ( 7) by propositional logic) This disqualifies KD45-based PAL as a logic of belief dynamics. It is currently not clear how this problem has to be addressed

Variants of PAL

Public Announcement Logic (PAL) turned out to be extremely fruitful. We briefly mention here some of its extensions in order to be able to refer to them in the sequel.

PAL being about epistemic actions only, it was extended by assignments in several papers [START_REF] Kooi | Expressivity and completeness for public update logic via reduction axioms[END_REF]106,114,115,117]. It was shown in the latter two papers that the epistemic extension of Reiter's solution to the frame problem [START_REF] Scherl | The frame problem and knowledge producing actions[END_REF][START_REF] Scherl | The frame problem and knowledge producing actions[END_REF] can be captured in the extension of DL-PA by epistemic operators and public announcements.

While PAL announcements are public, starting with [START_REF] Gerbrandy | Reasoning about information change[END_REF] several authors undertook to relax that hypothesis. Most prominently, dynamic epistemic logics [START_REF] Baltag | Logics for epistemic programs[END_REF] have event models which model that agents perceive events only incompletely.

Group Announcement Logic (GAL) is an extension of PAL by group announcements [2]. It actually blends PAL's announcements with an ATL-like ability operator involving a group of agents. The formula J ψ reads "J can achieve ψ by announcing some known formulas".

Arbitrary Public Announcement Logic (APAL) is an extension of PAL by arbitrary announcements [START_REF] Balbiani | Knowable'as 'known after an announcement[END_REF]. Formulas involving the latter take the form ! ψ and are read "there is a ϕ such that ϕ! ψ". APAL provides a formal framework for the analysis of the knowability paradox, also known as the Fitch paradox. The paradox-or rather, the problem-is that if we add to APAL the prima facie reasonable principle that all truths are knowable, formally

ϕ → ! K i ϕ, then ϕ → K i ϕ can be proved. Indeed, (ϕ ∧ ¬K i ϕ) → ! K i (ϕ ∧ ¬K i ϕ)
is an instance of the knowability principle whose right hand side is inconsistent because K i (ϕ ∧ ¬K i ϕ) is so in S5. In other words, while APAL is a conservative extension of PAL, the extension of APAL by the knowability principle fails to be a conservative extension of PAL and also of the underlying epistemic logic (unless the latter has ϕ → K k ϕ as a theorem). The satisfiability problem of APAL is undecidable [START_REF] French | Undecidability for arbitrary public announcement logic[END_REF]. In the next section we show that one cannot reason about uniform choices in APAL.

The problem of uniform choice in APAL

The problem of uniform choice was up to now only studied in logics with a strategic interpretation of actions. It however already occurs with nonstrategic action operators as soon as they quantify existentially over action choices. We call this the problem of uniform choice: the problem of how to express in the logical language that an agent knows how to achieve some ϕ. This implies that the agent also knows that there is a choice of his achieving ϕ, but not the other way round. Here is an example illustrating this in APAL.

Suppose you (Y ) know that there are only two cards, the ace of spades and the ace of diamonds. Bob (B) and Cath (C) each hold one of these two. You don't see B's and C's cards, and they only see their own cards; so if Bob holds the ace of spades then he does not know that the other card is an ace of diamonds, and so on. There are two alternative situations for you: one where Bob holds spades and Cath holds diamonds, and one where Bob holds diamonds and Cath holds spades; they are depicted in Fig. 1.

Suppose you want B to know C's card, but not the other way round. Is there a public announcement doing the job?

We start by describing the initial situation and the goal situation:

Init = K Y Spades ∧ K Y Diamonds ∧ K Y (K B Spades ∧ ¬K C Spades) ∨ (K B Diamonds ∧ ¬K C Diamonds) Goal = K B (Spades ∧ Diamonds) ∧ ¬K C (Spades ∧ Diamonds)
where Spades means that one of agents B and C holds the spades and similarly for Diamonds.

The following are theorems of PAL:

⊢ PAL (K B Spades ∧ ¬K C Spades) → Spades→Diamonds! Goal ⊢ PAL (K B Diamonds ∧ ¬K C Diamonds) → Diamonds→Spades! Goal
So if B holds the ace of spades then the announcement Spades→Diamonds! does the job; and if B holds the ace of diamonds then the announcement Diamonds→Spades! does the job. It follows that ⊢ APAL Init → K Y ∃! Goal: given the initial situation Init, you know that there is an announcement achieving the goal. However, you don't know which announcement you should make. Our example is a typical situation where you know that there is a strategy, but you don't know which action to choose. There seems to be no way to express in APAL that there is no uniform choice guaranteeing the goal. The problem can be solved in GAL, where one can write both K Y {Y } ϕ and {Y } K Y ϕ. The former says that you know that you have a (possibly non-uniform) choice achieving ϕ, while the latter says that you have a (necessarily uniform) choice of which you know that it achieves ϕ.

Individual knowledge, strategic actions: ATEL

We now briefly turn towards a paradigmatic logic of knowledge and strategic action: Alternating-time Temporal Epistemic Logic (ATEL) [109]. ATEL combines ATL with epistemic logic. It has formulas of the form [J ] ψ where ψ is a formula governed by a temporal operator just as in ATL (cf. Sect. 4.1), read "coalition J can achieve ψ (whatever its opponents do)", and K i ϕ, read "agent i ∈ I knows that ϕ".

It was pointed out by Schobbens that in ATEL one cannot represent uniform strategies [START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF]. The problem is basically the same as APAL's problem of uniform choice that we have exposed in Sect. 6.4, viz. to design a logical language allowing to express that an agent knows a strategy to enforce some property, which is stronger a statement than that the agent knows that there is a strategy; in the latter case he does not necessarily know what strategy to select. Indeed, it is irrelevant whether there is a quantification over the opponents' actions or not: the problem rather comes from the existential quantification occurring in the modal operators of ability. It may be exemplified in the language of ATEL by the formula K i [i] XSafeOpen which expresses that agent i knows that there is an action of his opening the safe: the formula may be true without agent i knowing the combination of the safe. Following Schobbens's paper, several amendments of ATEL where proposed in the literature in order to allow to express uniformity of strategies. It seems fair to say that the accounts they propose are fairly complex: Constructive Strategic Logic [START_REF] Jamroga | Constructive knowledge: what agents can achieve under imperfect information[END_REF] evaluates formulas not at state but at a set of states, leading to a non-standard negation operator; Alternating-time Temporal Observation Logic (ATOL) [START_REF] Jamroga | Agents that know how to play[END_REF] has formulas with indexed path quantifiers [J ] Obs(i) ψ "group J has a strategy to enforce ψ, and agent i can see the strategy".

Perhaps the most promising solutions are provided by extensions of ATL framework with strategic contexts. In the language of ATEL with Explicit Actions ATELEA [START_REF] Herzig | Alternating-time temporal logic with explicit actions[END_REF], which is the epistemic extension of logic ATLEA of Sect. 4.2, one might write for example K i [i] i:dial 1234 XSa f eO pen in order to express that i knows the combination of the safe. A further step in this direction is Epistemic Strategy Logic ESL [START_REF] Belardinelli | Reasoning about knowledge and strategies: Epistemic strategy logic[END_REF] where Strategy Logic SL is extended with epistemic operators.

It has also been proposed to solve the problem of uniform strategies by moving to an epistemic extension of the logic of agency STIT [START_REF] Broersen | Using STIT theory to talk about strategies[END_REF][START_REF] Broersen | What groups do, can do, and know they can do: An analysis in normal modal logics[END_REF][START_REF] Herzig | Knowing how to play: Uniform choices in logics of agency[END_REF]. The language of that logic has four kinds of modal operators: the epistemic operator K i , the historic possibility operator ♦, the agency operator Stit i , and temporal operators X etc. As we have said in Sect. 4.3, the sequence ♦Stit i X captures the ATL operator [i] X. The difference is that [i] X is a single, fused operator while in STIT it is decomposed into its three constituents. This provides a greater linguistic flexibility because the epistemic operator K i can be inserted anywhere in the sequence. First, the formula K i ♦Stit i Xϕ is what can be said in ATEL about agent i's de dicto knowledge, while the formula ♦K i Stit i Xϕ is about i's de re knowledge; it cannot be formulated in ATEL. In our example, the conjunction K i ♦Stit i X SafeOpen∧¬♦K i Stit i X SafeOpen adequately expresses that i knows that there is an action opening the safe, but does not know which action opens it: there no choice of an action for which i knows that i sees to it that the safe is open next. In the case of multiple agents the picture can be further refined by distinguishing i's ex ante knowledge-what i knows before choosing his action-, i's intermediate knowledge-what i knows given that he has chosen his action but does not know the other agents' choices-, and i's ex post knowledge-what i knows once all the agents' choices are known to him [START_REF] Lorini | A logical analysis of responsibility attribution: Emotions, individuals and collectives[END_REF].

Group knowledge, no actions: S5 CK

The concept of common knowledge is central in several disciplines. In the social sciences it is the basis of conventions [START_REF] Lewis | Convention: A philosophical study[END_REF]. In semantics it provides the notion of common ground in

EL

Some axiomatics of epistemic logic FP(CK J )

EK J CK J ϕ ↔ EK J (ϕ ∧ CK J ϕ) GFP(CK J ) EK J ϕ ∧ CK J (ϕ → EK J ϕ) → CK J ϕ
conversation [START_REF] Clark | Definite reference and mutual knowledge[END_REF]. In game theory, the hypothesis of common knowledge of rationality was proved to be fundamental for equilibria [START_REF] Aumann | Agreeing to disagree[END_REF]. In theoretical computer science it is used to study communication in distributed systems [START_REF] Fagin | Reasoning about knowledge[END_REF].

The language has common knowledge operators CK J , one per group J ⊆ I. The formula CK J ϕ is read "it is common knowledge in group J that ϕ".

As we have said in Sect. 2.1, common knowledge of ϕ, CK J ϕ, is typically explained in terms of the modal operator of shared knowledge EK J as being the infinite conjunction EK J ϕ ∧ EK J EK J ϕ ∧ EK J EK J EK J ϕ ∧ • • • . However, due to this infiniteness CK J cannot be syntactically reduced to EK J and requires a proper axiomatisation. Most of the axiomatisations in the literature are built on top of the epistemic logic S5. Given that we have stressed the inappropriateness of the latter as a logic of knowledge in Sect. 5.2, the axiomatics we give in Table 8 is based on a non-specified normal modal logic of individual knowledge EL that may be any modal logic between K and S5. It is obtained by adding two axioms to the logic of individual knowledge EL: the Fixpoint Axiom FP(CK J ) and the Greatest Fixpoint Axiom GFP(CK J ). Both involve shared knowledge EK J ϕ, which as we have mentioned in Sect. 2.1 abbreviates i∈J K i ϕ. Axiom GFP(CK J ) can be replaced by the following inference rule:

It can be proved that CK J is a normal modal operator. We observe that the formula

CK {1,2} ϕ 1 ↔ϕ 2 ∧ i∈{1,2} ϕ i →K i ϕ i → CK {1,2} ϕ 1 ∧ϕ 2 → EK {1,2} ϕ 1 ∧ϕ 2
is a theorem of EL CK if EL is a normal modal logic. It says that if it is common knowledge that ϕ 1 and ϕ 2 have the same truth value and that each agent i knows the truth value of 'his' ϕ i then it is common knowledge that if both are true then everybody knows this. Here is a proof.

We now study the extension of PAL by the common knowledge operator as a prototypical logic involving both group knowledge and nonstrategic actions. The dynamic dimension enables us to discuss what we believe to be a surprising and debatable consequence of the Greatest Fixpoint Axiom GFP(CK J ) of Table 8.

Public announcement logic with common knowledge PAL CK

Public Announcement Logic with Common Knowledge PAL CK is an extension of the logic of common knowledge by public announcements. It may as well be viewed as an extension of PAL by common knowledge. An axiomatisation of PAL CK can be found in [START_REF] Baltag | Logics for epistemic programs[END_REF]Fig. 9]. It extends the axiomatics of PAL of Table 7 by the following rule:

χ → ϕ! ψ (χ ∧ ϕ) → EK I ψ χ → ϕ! CK I ψ
The common knowledge version ψ! CK J ϕ ↔ ψ∧CK J [ψ!]ϕ of the reduction axiom Red(K i ) cannot be proved in PAL CK : while the right-to-left direction is a theorem, the left-to-right direction is not. So common knowledge may 'pop up' as a consequence of a public announcement in a way that is unforeseeable for the group J . In contrast, the reduction axiom Red(K i ) says that an agent can foresee what he will know after the announcement of ψ, namely what he currently knows to be true after the announcement of ψ. From a more general perspective, this means that the logical properties of the common knowledge operator differ from that of the individual knowledge operator, while these two operators obey exactly the same principles in the underlying epistemic logic: when the principles for K i are those of S5 then the principles for CK J are those of S5, too. Beyond such formal considerations, the sequel provides an example casting some doubt on the suitability of PAL CK as a logic of common knowledge and public announcements.

The ignorant compatriots example

We take over an example from [START_REF] Lorini | Direct and indirect common belief[END_REF]. Suppose agents B and C are both Italian, expressed by the conjunction it B ∧it C , and don't know each other. They accidentally meet in the coffee break of some conference and start to talk in English. It is commonsense knowledge-and by that also common knowledge of A and B-that each of them knows whether he/she is Italian or not. This is described by the following formula:

Init = it B ∧ it C ∧ i∈{B,C} CK {B,C} (it i →K i it i ) ∧ (¬it i →K i ¬it i ) .
However, B does not know that C is Italian and C does not know that B is Italian.

We consider two continuations of our story.

In the first scenario, a third agent who happens to know both of them overhears their conversation and truthfully declares: "Hey, you are both Italian!" By the announcement it clearly becomes common knowledge that both are Italian: we have

⊢ PAL CK Init → it B ∧it C ! CK {B,C} it B ∧it C .
In the second scenario, the third agent truthfully says: "Hey, you are compatriots!" Surprisingly, the principles of PAL CK tell us that it B ∧it C immediately becomes common knowledge, too:

⊢ PAL CK Init → it B ↔it C ! CK {B,C} (it B ∧it C ).
To see this, remember from Sect. 8 that it B ↔it C being boolean, we have

⊢ PAL CK it B ↔it C ! CK {B,C} (it B ↔it C ),
and that we have moreover

⊢ EL CK CK {B,C} it B ↔it C ∧ i∈{B,C} it i →K i it i → CK {B,C} it B ∧it C → EK B,C it B ∧it C .
Together with the instance

⊢ PAL CK it B ∧it C ∧ CK {B,C} it B ∧it C → EK {B,C} (it B ∧it C ) → CK {B,C} it B ∧it C of the Greatest Fixpoint Axiom GFP(CK J ) it follows that ⊢ PAL CK Init → CK {B,C} it B ∧it C .
This inference is however at least questionable: in real life conversations, agent B is able to infer from his knowledge that CK J it C →K C it C and the truthful public announcement

it B ↔it C ! that it B , K C it B , K C K B it B , K C K B K C it B ,
etc. are all true, up to any level of nesting; however, it seems that the announcement of it B ↔it C never makes it B ∧it C part of the common ground of the conversation. 5 One may argue that human agents may fail to infer all logical consequences in such a situation, just as they fail to infer the right conclusion in the case of other logical fallacies. However, we find it puzzling that the formal model of common knowledge does not match human reasoning in a simple situation with two agents and two propositions at stake.

It was proposed in [START_REF] Lorini | Direct and indirect common belief[END_REF] that one should distinguish two forms of common knowledge: implicit common knowledge and explicit common knowledge, with modal operators CK J and ECK J . Implicit common knowledge is PAL CK common knowledge: it has the least fixpoint axiom and there is no reduction axiom for it. In contrast, explicit common knowledge ECK J does not have the least fixpoint axiom (it is some fixpoint, but not necessarily the least) and has the following reduction axiom:

[ψ!]ECK J ϕ ↔ ¬ψ ∨ ECK J [ψ!]ϕ.
Let PAL CK,ECK be the resulting logic (for some underlying normal modal logic of individual knowledge EL). In the second scenario of our compatriots example we get the following two theorems:

⊢ PAL CK,ECK Init → it B ∧it C ! CK {B,C} (it B ∧it C ) ∧ ECK {B,C} (it B ∧it C ) , ⊢ PAL CK,ECK Init → it B ↔it C ! CK {B,C} (it B ∧it C ) ∧ ¬ECK {B,C} (it B ∧it C ) .
So the two operators lead to the same outcome in the first scenario, while we obtain two different outcomes in the second scenario, depending on the kind of common knowledge under consideration. It therefore seems that the modal operator ECK J might be more appropriate for example for reasoning about the common ground in conversation.

We contend that the above criticism is not as stringent as the others we have put forward up to now, which had a more formal nature. However, we believe that the standard account of common knowledge in terms of the least fixpoint axiom deserves to be questioned. Actually the issue brought up by our second scenario can be related to the omniscience problem: it illustrates that the inference of common knowledge that is delivered by the least fixpoint axiom is by no means guaranteed if agents have limited reasoning capabilities. The least fixpoint axiom has therefore to be considered as a further omniscience principle, to be added to those that we have listed for the individual knowledge operator in Sect. 5.1. The systematic failure of humans to infer common knowledge in our simple scenario indicates that it should actually be the first epistemic principle to be questioned when investigating the omniscience problem.

A remark on distributed knowledge

The extension of PAL by distributed knowledge has not been studied much, with the exception of [START_REF] Hansen | A hybrid public announcement logic with distributed knowledge[END_REF]122]. We do not discuss the issue here and refer the reader to the above papers. This is however the right moment to point out the shortcoming of our informal definition of distributed knowledge as 'knowledge achievable by communication'. This works for boolean formulas as well as for positive epistemic formulas: formulas without action operators and without epistemic operators in the scope of negation. It is inappropriate for Moore sentences such as p∧¬K i p. To see this consider the extension of Arbitrary Public Announcement Logic APAL of Sect. 6.3 by the shared knowledge operator and define "ϕ is distributed knowledge in the group of all agents I" as the formula ! EK I ϕ. Suppose I contains at least two agents i and j, and suppose j knows that p∧¬K i p. As individual knowledge implies distributed knowledge (cf. Sect. 2.1), p∧¬K i p must be distributed knowledge in I. However, p∧¬K i p cannot become knowledge of i, i.e., K i ( p∧¬K i p) is inconsistent in S5 (it is actually already so in the weaker logic KD4). It follows that p∧¬K i p cannot become shared knowledge of any group involving i and, a fortiori, not of I: the formula EK I ( p∧¬K i p) is inconsistent in S5 CK .

Similarly, in our scenario the formula p∧¬K i p cannot become common knowledge of I. So a more demanding definition of distributed knowledge as achievable common knowledge leads to a problem, too. The problem actually already shows up for a less demanding scenario where j knows that p∧¬CK I p.

This calls for further investigation of the interplay between announcements and distributed knowledge.

Group knowledge, strategic actions: ATEL CK

The grande finale of our presentation is the class of logics having both group knowledge and strategic actions. We focus on the extension of the logic ATEL of Sect. 7 by common knowledge, appropriately baptised ATEL CK .

The logic ATEL CK inherits all the problems of its fragments: as to the epistemic dimension, we have seen that we get in trouble if we choose S5 as the logic of knowledge and should choose S4.2 instead (cf. Sect. 5.2), which in turn leads to technical problems (cf. Sect. 6.2) and we have seen that the Greatest Fixpoint Axiom GFP(CK J ) might be too strong for common knowledge (cf. Sect. 9.2); as to the dynamic dimension, we have seen that ATL strategies lack commitments (cf. Sect. 4.2) and that ATEL does not enable us to reason about uniform choices and uniform strategies (cf. Sect. 7).

We do not want to discuss these problems again here. Instead, we briefly mention a further difficulty: when we want to say that a group J knows how to achieve some goal ϕ, i.e., that J knows that J has a strategy to achieve ϕ, then it is not clear which kind of group knowledge is required. Sometimes distributed knowledge DK J [J ] Fϕ is enough; sometimes shared knowledge EK J [J ] Fϕ is enough; and sometimes common knowledge CK J [J ] Fϕ is required. For example, the Byzantine agreement problem where communication is asynchronous and where messages may get lost requires common knowledge of a uniform strategy. In contrast, when public announcements can be made then distributed knowledge is enough. We believe that this is an interesting topic for further investigation.

Summary and research challenges

We have categorised logics for MAS in terms of the knowledge dimension and the action dimension, and for each category we have revisited and criticised its most prominent logics. As to logics with nonstrategic action operators, we have advocated DL-PA as an interesting logic that solves the frame problem and that embeds logics of nonstrategic ability. We believe it to be an appropriate basis for formal approaches to knowledge representation in general and to MAS in particular. Beyond the embedding of CL-PC that we have recalled in Sect. 3.5, the central role of DL-PA is confirmed by DL-PA accounts of update and revision operations [START_REF] Herzig | Belief change operations: A short history of nearly everything, told in dynamic logic of propositional assignments[END_REF], belief merging operations [START_REF] Herzig | Belief merging in dynamic logic of propositional assignments[END_REF], abstract argumentation theories and their modification [START_REF] Doutre | A dynamic logic framework for abstract argumentation[END_REF], and answer-set programs and their modification [START_REF] Del Cerro | Combining equilibrium logic and dynamic logic. Logic programming and nonmonotonic reasoning[END_REF]; moreover, its epistemic extension, public announcement logic with assignments, solves the epistemic frame problem [114,115]. As to logics with epistemic operators, we have recalled that S5 is inadequate as a logic of knowledge and should be replaced by S4.2; furthermore, we have shown that the definition of common knowledge by means of the Greatest Fixpoint Axiom GFP(CK J ) is at least questionable. Finally, as to logics with strategic action operators, we have shown that ATL has to be augmented by some notion of commitment (to an action or to a strategy) and that just as arbitrary public announcement logic (APAL), its epistemic extension is too weak to cover reasoning about uniform strategies.

Let us terminate by sketching and discussing some challenges for future research.

11.1 From logics of knowledge to logics of belief (including belief revision)

In Sect. 5.2 we have criticised the choice of S5 as the logic of knowledge. One may however hope that negative introspection is justifiable at least in some contexts. For example, the interpreted systems from which knowledge is defined in [START_REF] Fagin | Reasoning about knowledge[END_REF] naturally validate that axiom. It would be interesting to investigate under which circumstances the axiom is a reasonable assumption. As far as we know this has not been investigated up to now. The epistemic concepts of individual knowledge and group knowledge have doxastic counterparts, viz. the concepts of individual belief and group belief. Belief is actually more primitive a concept than knowledge, and many have tried to define the latter from the former. However, there is no consensus about their precise relationship apart from simple principles such as 'knowledge implies belief' that we have mentioned in Sect. 6.

The move towards beliefs comes with some new problems. The first difficulty is that while knowledge is binary-either you know or you don't-, belief typically comes in degrees. How this should be modeled and how degrees relate to (subjective) probability theory is an old and much debated subject of research. The second and main difficulty is that contrarily to knowledge, beliefs sometimes have to be revised: while knowledge is always true (because knowledge implies truth), an agent's beliefs may be false. In the context of PAL, an agent may wrongly believe that some announcement ψ cannot be made because he wrongly believes ψ to be false. In such circumstances only the left-to-right direction ψ!

B i ϕ → (ψ ∧ B i [ψ!]ϕ)
of the (belief version of the) reduction axiom Red(K i ) of Table 7 holds, and trivially so, while the right-to-left direction (ψ ∧ B i [ψ!]ϕ) → ψ! B i ϕ does not. A satisfactory doxastic version of PAL clearly has to integrate some notion of belief revision. How this should be done is still very much an open issue, despite numerous recent efforts [START_REF] Aucher | A combined system for update logic and belief revision[END_REF][START_REF] Aucher | Internal models and private multi-agent belief revision[END_REF]102,107,113]. In our view, a further problem that has not been addressed up to now in a satisfactory manner is that almost all belief revision theories presuppose some kind of preference information: in many cases it is not clear at all where this information comes from. In other words, the challenge is to find simpler, more modest theories of revision that can be easily and smoothly integrated into logics of belief and action. First steps in that direction can be found in recent papers, but much remains to be done [START_REF] Baltag | Group belief dynamics under iterated revision: Fixed points and cycles of joint upgrades[END_REF][START_REF] Baltag | Belief revision as a truth-tracking process[END_REF][START_REF] Baltag | The logic of justified belief, explicit knowledge, and conclusive evidence[END_REF].

Past artificial intelligence and MAS research on logics of knowledge and belief focussed a lot on the omniscience problem that we have mentioned in Sect. 5.1, probably because it was believed to be central in the implementation of BDI agents. We think the problem might have been overestimated a bit, while problems related to belief update and the analysis of plans were rather neglected in the implementation of BDI agents; see [START_REF] Alechina | Logic and agent programming languages[END_REF] for a similar point of view. Moreover, limited reasoning has often to be disregarded when we want to reason about opponents, for example when we model an attacker in a cryptographic protocol. Let us finally note that limited reasoning about common knowledge was not considered up to now in the literature on the omniscience problem. Our 'compatriots' example against PAL CK might be viewed as evidence that failure of application of the Greatest Fixpoint Axiom GFP(CK J ) should be the first thing to model in a satisfactory account of the multiagent omniscience problem.

Group belief and acceptance

Beyond individual belief, the investigation of different kinds of group belief is a highly interesting field of research. Examples are group acceptance and we-belief [105]. Acceptance is contextual: a lawyer accepts that his client is innocent in the context of the court, while he may privately believe that the client is guilty. As our law court example illustrates, neither does acceptance imply belief nor the other way round. In contrast, belief and we-belief are both non-contextual. We-belief differs from the standard notions of shared and common belief (whose knowledge counterparts were presented in Sects. 2.1 and 8) in that the latter two imply individual belief of the members of the group: for shared belief, the formula EB J ϕ → i∈J B i ϕ is a theorem, and for common belief CB J ϕ → i∈J B i ϕ is so. In contrast and just as group acceptance, we-belief does not imply individual belief: there may be a group belief in J that ϕ while some of the members of J don't believe that ϕ. For example, in the former Soviet Union there was a we-belief that the capitalist countries would perish soon, while only very little citizens individually believed this [105].

Failure to imply individual belief makes group acceptance and group belief relevant for the analysis of concepts such as reputation: an agent i may have a good reputation in group J although some members of J do not adhere to the group view. This was explored in [START_REF] Herzig | A logic of trust and reputation[END_REF] in order to provide a logical analysis of reputation. The logics of different kinds of group belief and their interrelations were recently investigated by several authors [START_REF] Gaudou | Grounding and the expression of belief[END_REF][START_REF] Hakli | Group beliefs and the distinction between belief and acceptance[END_REF][START_REF] Lorini | The logic of acceptance: Grounding institutions on agents' attitudes[END_REF]. One of the issues that are essentially left open in these approaches is the relation between different contexts: in the existing proposals they are unanalysed objects.

Logic of action

As its name indicates, PAL presupposes that announcements are perceived correctly and completely by all agents. We have mentioned in Sect. 6.3 that Baltag et al.'s event models provide an elegant generalisation where the agents' perception of the action is modelled by means of a Kripke model whose points are possible events and where the possible events a and b are related by the accessibility relation for agent i if and only if a and b are indistinguishable for i [START_REF] Baltag | Logics for epistemic programs[END_REF]. This gave rise to a flourishing research avenue that was baptised dynamic epistemic logics. We believe that its version with assignments as designed in [117] provides a promising basis for a unified logic allowing for reasoning about non-strategic action in MAS.

While being theoretically elegant, event models are rather intricate to handle when modelling applications where there are few agents who perceive an action while most of the agents don't, which is a typical situation for example in cryptographic protocols. This is due to the occurrence of event models in the language of the logic as such: the language provides no other means to talk about actions. This is at odds with the idea of syntactic knowledge representation that we have followed in our presentations. It is also not clear how an appropriate language not incorporating such a semantical devices can be designed. First steps are in [START_REF] Aucher | Perspectives on belief and change[END_REF]116] which propose syntactical constructions that are interpreted in event models. The recent paper by Hales et al. [START_REF] Hales | A composable language for action models[END_REF] establishes that such a language can be built from Gerbrandy's logic of private announcements [START_REF] Gerbrandy | Reasoning about information change[END_REF] together with the PDL program operators.

We have mentioned in Sect. 4.2 that there is currently a lot of activity around strategic reasoning, with a dedicated workshop series that started in 2013. A major challenge is to tame complexity. Beyond extensions and fragments of strategy logic, a further interesting research avenue is to provide such results for stit logics that were mentioned in Sect. 7 as a framework for reasoning about uniform strategies. Some decidability results are in [START_REF] Schwarzentruber | Complexity results of STIT fragments[END_REF].

Logic of goals (including group goals)

In the introduction we have mentioned three fundamental concepts in MAS: knowledge, actions and goals. However, in the present paper we did not talk at all about logics of goals, nor about logics for the closely related concept of intention. One of the reasons for that is that there is far less consensus here than about logics of knowledge and action. It is a major challenge to provide logics improving that state of affairs. Just as in the case of group beliefs, one of the most important issues is to logically analyse the relation between group goals and individual goals. More generally, what remains to be done is an integration of so-called belief-desire-intention (BDI) logics [START_REF] Cohen | Intention is choice with commitment[END_REF][START_REF] Cohen | Persistence, intentions, and commitment[END_REF] with strategic logics such as ATL. First steps are in [123].

The relation with game theory

Game theory is seen by many as the most prominent theory of interaction between rational agents. Some of the logics that we have presented have strong links with game theory: ATL, CL and STIT have semantic structures that were taken over from game theory. A challenge for future research is to integrate into these logics the notion of utility. First steps in this direction were undertaken recently by several researchers, typically encoding utilities by means of special propositional variables [START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract)[END_REF][START_REF] Lorini | On the epistemic foundation for iterated weak dominance: An analysis in a logic of individual and collective attitudes[END_REF][START_REF] Lorini | A modal logic of epistemic games[END_REF]107]. A more principled approach should involve an analysis of the notion of goal, which brings us back to the preceding challenge.

We note that there is also a sort of mismatch that remains to be investigated: while Bratman, Cohen & Levesque and others have forcefully argued that logics of belief and goal should be augmented by the concept of future-oriented intention-leading to BDI logics [START_REF] Cohen | Intention is choice with commitment[END_REF][START_REF] Cohen | Persistence, intentions, and commitment[END_REF])-, game theory in its current state does not include such a concept. It therefore remains to be investigated whether the concept of intention could enrich game theory or not.

A general technical problem

Let us terminate on a more general note. As is always the case when modelling real-world problems, there is a delicate balance between conceptual richness and mathematical complexity. Each of the logics of knowledge and action that we have presented is a multi-dimensional modal logic: a product logic or a semi-product [START_REF] Gabbay | Many-dimensional modal logics: Theory and applications[END_REF]. Such logics are often undecidable, and when they are decidable then they are in general very complex. This is not a problem as long as one only wants to model some application. However, as soon as one aims at the mechanical verification of MAS specifications then decidability and complexity become relevant. We believe that one should then start from a very simple logic of action and a very simple logic of knowledge. In this paper we have advocated DL-PA as a simple yet powerful logic of action. Perhaps models of knowledge where knowledge is based on an underlying relation of 'propositional perception' where an agent only sees the truth value of some propositional variables [111] is a good starting point for a simple logic of knowledge.

  [J] ) and M( [J] ) do not appear in the original presentation, while [∅] G⊤ and the inference rulesϕ [∅] Gϕ and ϕ → ψ [∅] Xϕ → [∅] Xψare missing in ours. The first can be proved from N([J] ) via RE( [J] )and the Greatest Fixpoint Axiom GFP(G). The second can be derived from the first via RE( [J] ). The third can be derived from M( [J] ) via RE( [J] ).

4. 3

 3 Seeing-To-It-That Logic (STIT) While PDL and ATL are about what agents can do, STIT [19,64] is both about what agents can do and about what they actually do. Such logics are called logics of agency in the philosophy of action literature. We here present the so-called Chellas STIT version.

Fig. 1

 1 Fig. 1 Two possible alternative situations for agent Y

Table 1

 1 The modal operators of knowledge Type of operator Notation Reading

Table 2

 2 The modal operators of ability and action

	Type of operator	Notation	Reading
	Nonstrategic	π ϕ	"Action π can achieve ϕ if the other agents do nothing",
			"There is an execution of program π after which ϕ"
		J ϕ	"Group J can achieve ϕ while the other agents don't act"
	Strategic	[J ] ψ	"Coalition J can achieve ψ whatever the opponents do"
		Stit J ϕ	"Coalition J achieves ϕ whatever the opponents do"

Table 3

 3 The grid of MAS logics

		Knowledge
	Action	No actions	Nonstrategic action	Strategic action
	No uncertainty		CL-PC; PDL	ATL; STIT
	Individual knowledge	S5	PAL	ATEL
	Group knowledge	S5 CK	PAL CK	ATEL CK

Table 4 is about the PDL program operators. Its schemas Seq, Nondet, and Test are equivalences without program operators on the right. It follows that for the star-free fragment, all program operators can be eliminated. For the iteration operator * there are two axioms: FP( π * ) is a fixpoint axiom and LFP( π * ) is a least fixpoint axiom

 4 . When ϕ is deducible from Γ in PDL we write Γ ⊢ PDL ϕ. The following version of the deduction theorem holds:

Table 4

 4 Axiomatisation of PDL RE

Table 6

 6 Axiomatisation of the epistemic logic S5 RE

Table 7

 7 Axiomatisation of PAL

	EL	Some axiomatics of epistemic logic
		(e.g. S5 of Table

Table 8

 8 Axiomatisation of epistemic logics with common knowledge EL CK

The set of agent names cannot be infinite if we want the set of all groups of agents to be enumerable-for example, if I were allowed to be the set of natural numbers then the set of subsets of I would be uncountable-, and enumerability is necessary to obtain finite axiomatisations. Another way out is to only consider finite subsets of an infinite set of agents. We refer to[START_REF] Halpern | Reasoning about common knowledge with infinitely many agents[END_REF] for non-finite axiomatisations of logics of group knowledge.

We have chosen the notation [J ] -the nesting of a modal diamond and a modal box-in order to signal a ∀∃ quantification. It is however not standard in the literature, where one can find J in Pauly's Coalition Logic CL and J in Alternating-time Temporal Logic (ATL).

We here give a simplified version; the original formulation is not about the above extension PDL ∀ of PDL, but about logic ES[START_REF] Lakemeyer | A semantic characterization of a useful fragment of the situation calculus with knowledge[END_REF]. The latter is a variant of the Situation Calculus where situation terms are suppressed (and which is therefore closer to modal logics) and which moreover comes with sensing actions and epistemic operators.

Thanks are due to Nicholas Asher for a confirmation of that point in conversation.

Acknowledgments

The ideas in this paper were presented in an invited talk at the 2013 International Joint Conference on Artificial Intelligence (IJCAI 2013) that was entitled "Logics for multiagent systems: a critical overview". It is based on joint work with several colleagues that I would like to thank here for our smooth and fruitful collaboration: Philippe Balbiani (U. Toulouse, CNRS), Jan Broersen (U. Utrecht), Hans van Ditmarsch (U. Nancy, CNRS), Benoit Gaudou (U. Toulouse), Tiago de Lima (U. Artois, CNRS), Emiliano Lorini (U. Toulouse, CNRS), Faustine Maffre (U. Toulouse), Frédédric Moisan (U. Toulouse), François Schwarzentruber (U. Rennes, ENS), Nicolas Troquard (CNR, Trento), Dirk Walther (U. Politecnica de Madrid/U. Dresden). The overview presented in this paper is part of the efforts of the SINTELNET network (www.sintelnet.eu) to reexamine the logical foundations of concepts that are commonly used in artificial intelligence and the social sciences.