# common_knowledge_of_abstract_groups__4818aa8d.pdf

Common Knowledge of Abstract Groups

Merlin Humml, Lutz Schr oder

Friedrich-Alexander-Universit at Erlangen-N urnberg, Erlangen, Germany {merlin.humml, lutz.schroeder}@fau.de

Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in it is common knowledge among economists . We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge operator for groups of agents given by concepts in a separate agent logic that we keep generic, with one possible agent logic being ALC. We show that AGEL is EXPTIMEcomplete, with the lower bound established by reduction from standard group epistemic logic, and the upper bound by a satisfiability-preserving embedding into the full µ-calculus. Further main results include a finite model property (not enjoyed by the full µ-calculus) and a complete axiomatization.

Introduction Epistemic (modal) logic is concerned with the individual and collective knowledge of agents. One of the most important modalities for collective knowledge is common knowledge: A fact ϕ is common knowledge in a given group of agents if everyone in the group knows ϕ, and everyone knows that everyone knows ϕ, etc. In the present work, our focus of attention is on the involved notion of group of agents. The most basic variant of the common knowledge operator, typically written C, refers to all agents in a predetermined finite set Ag that forms a parameter of the logic as a whole (Fagin et al. 1995). In a more fine-grained variant, C can be annotated with an explicitly given subset of the set of agents: For A Ag, CAϕ says that ϕ is common knowledge among the agents in A. For instance, if Alice and Bob are legitimate participants in a communication protocol and ϕ is a fact concerning a shared key, then ϕ would ideally be common knowledge of Alice and Bob but not of a malicious third party Charlie i.e. C{Alice,Bob}ϕ would hold but C{Alice,Bob,Charlie}ϕ would not. Listing agents in a group explicitly is appropriate in wellcontrolled settings such as the above, where the participants in the epistemic situation are fixed and previously known. In other application contexts, however, this may not always be the case, in particular in statements found in real-world

Copyright 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

argumentation. Consider, for example, the sentence Doctors agree that smoking is bad for your health. We take this sentence (maybe debatably) as making a statement about common knowledge of all doctors. Encoding this claim as a formula of the form CAϕ where A is a finite set explicitly enumerating all doctors is clearly neither feasible nor even semantically desirable, as the statement is presumably meant to hold without regard to exactly how many, and which, doctors are practising in the world at the moment. Rather, one would want A to be given by the defining property of being a doctor.

In the present paper, we introduce an epistemic logic that allows precisely this: abstract-group epistemic logic (AGEL) features a common knowledge operator for groups of agents described by concepts in a dedicated agent logic. We keep the technical development generic in the choice of agent logic, subject to some technical requirements on the agent logic that are satisfied, for instance, by the description logic ALC; so we can describe groups of agents such as doctors and pharmacists or parents of teenagers . We note that we treat the agent logic as rigid, i.e. there is no uncertainty about membership in the groups it describes. In other words, group descriptions are de re rather than de dicto. We further illustrate the logic on a variant of the muddy children puzzle where the number of participants is unspecified and potentially large. Our main results on AGEL are EXPTIME-completeness of the satisfiability problem; a bounded (specifically, doubly exponential) model property; and a complete axiomatization. Technically, we establish the lower complexity bound by a satisfiabilitypreserving translation of standard group epistemic logic (Fagin et al. 1995) into AGEL, and the upper bound by a satisfiability-preserving translation of AGEL into the full µ-calculus (i.e. ALC with inverse roles and fixpoint operators (Vardi 1998)). Use of the full µ-calculus avoids the exponential blow-up that would be incurred by a more naive reverse translation of AGEL into group epistemic logic. However, the full µ-calculus does not have the finite model property (Vardi 1998; Streett 1982). Instead, we show the bounded model property and completeness by means of a filtered model construction that uses ideas from the finite model construction for propositional dynamic logic (Fischer and Ladner 1979; Blackburn, de Rijke, and Venema 2001), in particular transitive closure of (small) canonical pseudo-

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

models. Complete proofs can be found in the full version (Humml and Schr oder 2022).

Related Work There is a line of research on indexing knowledge modalities with names that designate groups of agents (Grove and Halpern 1993) (Fagin et al. 1995, Chapter 6). We refer to such groups as named groups; they are similar to the atoms of our agent logic but are non-rigid, i.e. their interpretation depends on the current world, in an approach that is focused on the analysis of knowledge about the identity of agents. Although common knowledge of such name-defined groups has been mentioned early on (Grove and Halpern 1993), results have largely focused on operators of the type every agent / some agent with name n knows (recall that generally, everyone knows ϕ differs from ϕ being common knowledge in that it need not imply that everyone knows that everyone knows ϕ, etc.). Recently, B ılkov a, Christoff, and Roy (2021) have shown completeness and the finite model property (but no complexity bound) for common knowledge of name-defined groups. (A different form of common knowledge for non-rigid groups has been considered earlier, without considering axiomatization (Moses and Tuttle 1988).) Extending the descriptive means for groups of agents has been considered already by Grove and Halpern (1993), who give an axiomatization (but no complexity bound) of a logic that features everyone knows and someone knows operators for propositional combinations of names. Additional expressive means are provided by subsequent firstorder extensions of the logic that allow quantifying over agent names (Grove 1995; Naumov and Tao 2019) in the style of term modal logic (Fitting, Thalmann, and Voronkov 2001). Quantifying over agents provides a straightforward way of encoding, e.g., the everybody knows operator ; for instance, every doctor knows ϕ would be expressed as x. doctor(x) Kxϕ if Kx denotes the usual single-agent knowledge modality x knows . Common knowledge, on the other hand, involves transitive closure and as such is not first-order expressible, hence not easily accommodated in such frameworks. Also, decidability results in a firstorder setting will, of course, require additional restrictions (e.g. it has recently been shown that the two-variable fragment of term-modal logic is decidable, with complexity between NEXPTIME and 2EXPSPACE (Padmanabha and Ramanujam 2019)). The above logics and ours employ ternary transition relations relating agents to pairs of worlds. Beyond epistemic logic, ternary relations appear, e.g., in the logic of Pierce algebras (de Rijke 1993), in arrow logic (Venema 1996), and in Routley-Meyer-style semantics of relevance logic (Mares 2020). While such modalities are formally similar to everyone-knows modalities for abstract groups, the frame conditions imposed on models and, consequently, the attached meta-theory are quite different from ours.

Abstract-Group Epistemic Logic We proceed to introduce the syntax and semantics of abstract-group epistemic logic (AGEL). Details and proofs

are often omitted or only sketched; a full version can be found on ar Xiv https://arxiv.org/abs/2211.16284.

Syntax We parametrize the logic over the choice of an agent logic LAg that serves to specify groups of agents. We will discuss assumptions on the semantics of LAg later in this section. Syntactically, we require only that LAg has a formula syntax where formulae are expressions in some grammar, in particular giving rise to a standard notion of subformula, and includes propositional atoms from a set At Ag, referred to as agent atoms, as well as the full set of Boolean connectives. Properties of LAg needed in our main results will be named explicitly in the respective theorems. One choice for LAg that satisfies all requisite properties is the standard description logic ALC (Baader et al. 2003). We further assume a set At W of world atoms. The set of (world) formulae ϕ, χ, . . . of AGEL is then defined by the grammar

ϕ, χ := | p | ϕ | ϕ χ | Cψϕ (p At W, ψ LAg).

That is, we include propositional atoms and Boolean connectives; further Boolean connectives , , are defined as usual. The key feature is then the common knowledge operator Cψ for groups of agents defined by an agent formula ψ; a formula Cψϕ is read ϕ is common knowledge among agents satisfying ψ , using the term common knowledge in the sense recalled in the introduction. Example 1. We may encode the statement parents of teenagers know that education is pointless as the AGEL formula C has Child. Teenager ep, using ALC as the agent logic and understanding the world atom ep as education is pointless . The even more frustrating fact that parents know that their offspring know this as well would be captured by the formula C has Child. Teenager CTeenager ep.

Semantics We assume that the agent logic comes with a notion of agent model, and that every agent model A is equipped with an underlying set Ag of agents and a satisfaction relation |=A Ag LAg; we write A, a |= ψ for (a, ψ) |=A, and JϕKA = {a Ag | A, a |= ψ}. We require that LAg conservatively extends classical propositional logic. By this we mean more specifically that LAg does not impose restrictions on valuations of agent atoms, i.e. given a set Ag and a valuation VAg: At Ag P(Ag), there always exists an agent model A with underlying set Ag such that A, a |= q iff a VAg(q), for a Ag and q At Ag. Then, an (AGEL) model M = (X, A, VW, ) consists of a set X of worlds, an agent model A, a world valuation VW: At W P(X) interpreting the world atoms, and a family of indistinguishability relations a X X indexed over agents a Ag. We require that each a is an equivalence relation (in keeping with the usual view that epistemic indistinguishability relations should be equivalence relations); see however Remark 3. For a set A Ag of agents, we write A= (S a A a) 1 where ( ) denotes reflexive-transitive closure (note that A is symmetric,

1This should not be confused with similar notation used to denote the intersection of the a in work on epistemic logic with quantification over agents (Naumov and Tao 2019)

hence an equivalence). We define satisfaction M, x |= ψ (x satisfies ψ) of a formula ψ at a world x recursively by

M, x |= M, x |= p iff x VW(p) M, x |= ϕ iff M, x |= ϕ M, x |= ϕ χ iff M, x |= ϕ and M, x |= χ M, x |= Cψϕ iff whenever x JψKA y, then M, y |= ϕ;

that is, Cψ is the standard box modality for JψKA. When M, x |= ϕ, then we also say that (M, x) is a model of ϕ (and we will use this phrasing in general, also for other logics). The formula ϕ is satisfiable if there is a model of ϕ, and valid (notation: |= ϕ) if M, x |= ϕ for all M, x. We write JϕKM = {x X | M, x |= ϕ}. We record a fixpoint characterization of Cψ:

Lemma 2. The set JCψϕKM is the greatest fixed point of the function F: P(X) P(X) given by F(U) being the set of worlds x such that M, x |= ϕ and whenever A, a |= ψ and x a y, then y U.

Remark 3. Since the modality Cψ takes reflexive-transitive closures, it is in fact immaterial whether the indistinguishability relations a are individually reflexive and transitive; we impose the corresponding requirement mainly to ease notation and discussion.

Remark 4. In logical settings with non-rigid (i.e. worlddependent) agent models (e.g. (Grove and Halpern 1993; Grove 1995; Naumov and Tao 2019)), one can accommodate uncertainty about the identity and properties of agents, and moreover specify agent groups by their knowledge, as in people who know ϕ also know ψ . As indicated in the introduction, AGEL, which assumes the agent logic to be rigid, trades this mode of expression for a computationally and axiomatically tractable treatment of common knowledge. One may still envisage extending AGEL with an operator I, with I ϕ read as knows about the truth or falsity of ϕ . That is, an agent satisfies I ϕ if in every world, she knows either ϕ or ϕ. For instance, if ϕ represents the publicly contested fact whether or not transfer negotiations are under way concerning a football player P, then I ϕ would hold for the relevant officials of the involved clubs and maybe for P. However, harnessing such an operator technically is likely to be challenging. To name one potential obstacle, the first-order translation of I ϕ would presumably need to involve three variables (i.e. unlike the translation of most modal logics would not end up in the two-variable fragment): one for the agent x, and two for worlds that are indistinguishable for x, and then required to agree on ϕ (see the appendix).

Remark 5. Since AGEL is effectively a fixpoint logic, it is expected that compactness fails. Indeed, given atomic agent concepts A, B and a world atom p, the set consisting of the formula CA B p and all formulae of the form CD1CD2 . . . CDnp, for n 0 and D1, . . . , Dn {A, B}, is unsatisfiable but all its finite subsets are satisfiable. It follows that there is no finitary proof system for AGEL that is strongly complete, i.e. makes all unsatisfiable sets of formulae inconsistent. We later give a proof system that is weakly complete, i.e. derives all valid formulae.

Complexity We show next that the satisfiability problem of AGEL is EXPTIME-complete.

Lower Bound: Reduction from Group Epistemic Logic We prove EXPTIME-hardness by a satisfiability-preserving encoding of standard group epistemic logic (GEL) (with common knowledge), which is known to be EXPTIMEhard (Fagin et al. 1995). (To facilitate the subsequent discussion, we reduce from a slightly more expressive logic than strictly necessary for the hardness proof.) We briefly recall the syntax and semantics of GEL: The logic is parametrized over a finite set Ag of agents and a set At W of (world) atoms. The set of formulae ϕ, ψ, . . . of GEL is then given by the grammar

ϕ, ψ ::= | p | ϕ | ϕ ψ | CGϕ

where p At W and = G Ag, with CGϕ read ϕ is common knowledge among the agents in G . (Knowledge operators Ka for individual agents a are included as common knowledge operators C{a}.) As indicated in the introduction, the difference with AGEL is that in GEL, groups G of agents need to be given as enumerated finite subsets of a known fixed set of named agents. Models M = (X, VW, ) consist of a set X of worlds, a (world) valuation VW: At W P(X), and a family of indistinguishability relations a X X, indexed over agents a Ag and again required to be equivalence relations. For G Ag, we write G:= (S a G a) . Then, satisfaction M, x |= ϕ of a formula ϕ at a world x is defined recursively by the expected clauses for atoms and propositional connectives, and

M, x |= CGϕ iff whenever x G y, then M, y |= ϕ.

The encoding q of GEL into AGEL is given as follows. We introduce a fresh agent atom pa for each a Ag. For a GEL formula ϕ, q(ϕ) is then defined recursively by

q(CGϕ) := CW

and commutation with all other constructs (i.e. q( ϕ) = q(ϕ) etc.). Using the running assumption that LAg conservatively extends classical propositional logic, we obtain Theorem 6 (Lower complexity bound). The satisfiability problem for AGEL is EXPTIME-hard.

Proof sketch. We need to show that q is indeed satisfiabilitypreserving. A model (M, x) of a GEL formula ϕ over the set Ag of agents, with M = (X, VW, ), is transformed into a model (M , x) of the AGEL formula q(ϕ), with M = (X, A, VW, ), by taking Ag to be the underlying set of A, and VAg(pa) = {a} for a Ag; this uses the running assumption that LAg conservatively extends classical propositional logic. Conversely, a model (M, x) of q(ϕ), with M = (X, A, VW, ), is transformed into a model (M , x) of ϕ, with M = (X, VW, ), by taking a = VAg(pa) (using notation like in the formal semantics of AGEL).

Remark 7. Depending on additional restrictions on the agent logic, it will sometimes be possible to give also a fairly straightforward satisfiability-preserving translation in the reverse direction, from AGEL to GEL. For instance, if the agent logic is just classical propositional logic, then we can proceed as follows: Let ϕ be an AGEL formula, and let A At Ag be the set of agent atoms mentioned in ϕ. Let Ag be the (finite) set of truth valuations κ: A 2 in the set 2 = { , } of Boolean truth values, and write κ(ψ) for the truth value of a propositional formula ψ over A under κ; then a translation of ϕ into a satisfiability-equivalent GEL formula s(ϕ) is defined recursively by

s(Cψχ) = C{κ Ag|κ(ψ)= }s(χ)

and commutation with all other constructs. However, even in this basic case, such a translation will be of limited use as it has exponential blowup (the set {κ Ag | κ(ψ) = } can be exponentially large). For more expressive agent logics, e.g. whenever the agent logic extends ALC, one has (series of) formulae that are satisfiable only over exponentially large agent models: Given agent formulae ψn that are of polynomial size in n but satisfiable only over agent models of exponential size in n (in ALC, such ψn exist), the AGEL formulae p Cψn p are satisfiable only over models whose agent model components are of exponential size in n. Indeed, from a purely computational point of view (and for suitably restricted agent logics), one may see AGEL as a way of dealing with exponentially many agents without incurring doubly exponential computational cost. We realize this by an encoding into a different target logic, discussed after the next example.

Example 8 (Lots of muddy children). The classical muddy children puzzle with k many children can be seen as k many agents Ai communicating according to a fixed protocol to gain common knowledge of a length-k bitstring where each agent Ai can see all bits except the one at index i (Pavlovic 2021, Section 4.3). Specifically, it is commonly known initially that at least one bit is set, and the protocol then proceeds in rounds in which the agents announce whether they have learned their missing bit. The full modelling of the puzzle thus requires a dynamic epistemic logic with common knowledge and public announcements (Baltag, Moss, and Solecki 1998; Lutz 2006). Here, we concentrate on modelling, in an extended setting, how knowledge is gained in individual rounds of the protocol, which does not require public announcements; we generalize the textbook treatment by Huth and Ryan (2004). We consider a variant of the puzzle that can essentially be seen as a product of n copies of the original puzzle. We then have an n k-matrix of bits, and each agent has an invisibility type consisting of one invisibility index per row determining the bit she cannot see in that row (in the original puzzle, there is only one row, and the invisibility type is the identity of the agent). We require that every bit of the matrix is seen by at least one agent. We do not otherwise restrict which invisibility types are realized; also, a given invisibility type may be realized by more than one agent. Note that there are exponentially many (viz, kn) invisibility

types; the point of these considerations being that the number of (distinguishable) agents is a) not fixed, and b) potentially large. We introduce propositional atoms p(j,i) for 1 j n and 1 i k indicating whether the bit at position (j, i) in the matrix is set (1). We use agent atoms hj,i to describe agents who cannot see the value of the bit at position (j, i) of the matrix, in an agent logic that extends propositional logic with a propositional background theory, in this case hardwiring the above description of the scenario (every agent sees all bits except one per row, and every bit is seen by some agent). The common knowledge resulting from the visibility conditions is hence

C ( V ij(pj,i C hj,ipj,i) ( pj,i C hj,i pj,i)).

We write α x j for the (purely propositional) formula stating that at most x bits are set in row j; that is, α x j is the disjunction of all conjunctions of the form V i H pi,j V i {1,...,k}\H pj,i where H {1, . . . , k} and |H| x. (This formula is of exponential size in the number k of columns, but note that this happens already in the original muddy children puzzle, i.e. in the case n = 1.) The initial knowledge available to the agents before the first round is that at least one bit is set in each row:

C (V j α 0 j ).

In each communication round the agents then choose one row, and communicate whether or not they know the value of the bit they cannot see in that row. Assuming all agents do not know the value of their respective bit, this establishes common knowledge about everyone s uncertainty:

C (V ij Chj,ipj,i Chj,i pj,i).

Of course the order of rounds is irrelevant here, and the state of the protocol can hence simply be represented by a tuple (xi, . . . , xn) where each xj counts how many communication rounds have taken place for row j (counting communication of the initial knowledge that at least one bit is set in each row). The key invariant of the protocol is that if these counters reach (x1, . . . , xn) without anyone having learned new bits, then this results in the accumulated common knowledge C (V j α xj j ).

This clearly holds in the beginning of the game due to the initial knowledge. Then in state (x1, . . . , xn), after querying row j, the common knowledge increases according to the inference

Γ, C ( α xj j ), C (V

i Chj,ipj,i Chj,i pj,i)

C ( α xj+1 j ).

where Γ represents the visibility axioms and denotes local (i.e. per-world) consequence.. The formal proof is similar to the textbook proof for the original puzzle (Huth and Ryan 2004), and sketched as follows:

Assume α xj+1 j .

From the accumulated knowledge of the previous rounds, the agents already know that more than xj bits are set in row j. From the assumption, they can conclude that exactly xj + 1 bits are set. Given that nobody knew whether their respective missing bit in row j is set, the agents can conclude that more than xj +1 bits are set in row j, contradicting the assumption. (Otherwise at least one agent whose bit is set would see only xj many set bits and could hence have deduced that her missing bit is set.)

Similar reasoning is used to conclude missing bits once enough communication rounds have been performed.

Upper Bound: Encoding into the Full µ-Calculus

We establish the EXPTIME upper bound on satisfiability checking by a satisfiability-preserving translation of AGEL into the µ-calculus with converse, also known as the full µcalculus, whose satisfiability problem is in EXPTIME (Vardi 1998). We emphasize that the full µ-calculus does not have the finite model property (Vardi 1998; Streett 1982); we therefore establish a bounded model property separately in the next section. In the translation, we use fixpoints to take transitivereflexive closures, and inverse roles to close under symmetry. The main idea is then to view the family of per-agent indistinguishability relations a featuring in the definition of AGEL models as a ternary relation on a single domain, and to encode this ternary relation as a binary relation between worlds and (agent, world)-pairs. In fact, the single-variable fragment of the full µ-calculus suffices for the translation; we briefly recall its syntax and semantics. The syntax is parametrized over sets AP and Prog of atomic propositions and atomic programs, respectively. A program is either an atomic program or a converse program α of α Prog. Moreover, we fix a single fixpoint variable z. Then, the set of formulae ϕ, ψ, . . . is given by the grammar

ϕ, ψ ::= | p | z | ϕ | ϕ ψ | [α]ϕ | νz. ϕ

where p AP and α is a program. The box operator [α] is read for all α-successors . The νz operator takes greatest fixpoints, and binds z; that is, an occurrence of z is free if it lies outside the scope of any νz. Application of νz is restricted to formulae ϕ in which every free occurrence of z is positive, i.e. lies under an even number of negations . Further propositional connectives , , , are defined as usual. Moreover, we define diamond operators as α ϕ := [α] ϕ. (Also, one can define least fixpoints µz. ϕ.) The semantics is defined over models M = (X, R, V ) that consist of a domain X, an assignment R of a transition relation R(α) X X to every atomic program α Prog; and a valuation V : AP P(X) of the atomic propositions. The interpretation of converse programs is defined by R(α ) = {(e, d) | (d, e) R(α)}. The semantics of a formula ϕ is then given as a function JϕKM: P(X) P(X) whose argument serves as the extension of z, inductively defined by the expected clauses for Boolean operators,

Jp KM = V (p), and

Jz KM(U) = U J[α]ϕKM(U) = {w X | v X. (w, v) R(α) v JϕKM(U)}

Jνz. ϕKM(U) = [ {Z X | Z JϕKM(Z)}.

One shows by induction that when νz. ϕ is well-formed, then JϕKM is monotone w.r.t. set inclusion, so Jνz. ϕKM(U) as defined above is, by the Knaster-Tarski fixpoint theorem, the greatest fixpoint of JϕKM. In detail, the translation is then defined as follows. We assume for the translation that the agent logic is given as a fragment of the full µ-calculus. For clarity, we write u for the syntactic embedding; we assume that each u(ψ) is closed, i.e. does not contain a free occurrence of z. As indicated previously, a typical choice would be ALC (modulo the usual slight syntactic shifts), but for purposes of the complexity analysis, the agent logic could in fact be the full µcalculus itself (whereas the axiomatization introduced in the next section needs assumptions on the agent logic that are not satisfied by the full µ-calculus, such as the finite model property). We use three fresh atomic programs π1, π2, edge. The intention is that edge relates worlds to (agent, world)-pairs, out of which π1 extracts the agent component, and π2 the world component. Speaking more precisely, we do not insist that π1, π2 are functional, so when (x, r) R(edge) in a model, then r may in fact represent several (agent, world) pairs, namely all pairs (a, y) such that (r, a) R(π1) and (r, y) R(π2) (and indeed it may happen that r represents no pair at all). As per Remark 3, we do not need to worry at this point about the fact that the induced indistinguishability relations are not forced to be equivalence relations. As an intermediate step in the translation, we introduce forward and backward binary next-step modalities by abbreviation:

ψ ϕ := [edge]( π1 ψ [π2]ϕ),

is understood as all worlds that are reached by a single forward indistinguishability step for an agent satisfying ψ satisfy ϕ , and

ψ := [π 2 ]( π1 ψ [edge ]ϕ)

describes the opposite direction, all worlds that are reached by a single backward indistinguishability step for an agent satisfying ψ satisfy ϕ . Using these two abbreviations to model a step along the symmetrization of the indistinguishability relation, we can encode the common knowledge modality, modelling transitive-reflexive closure via a greatest fixpoint as indicated above: We define the translation t of a AGEL formula ϕ into a formula t(ϕ) in the full µ-calculus recursively by

t(Cψϕ) = νz. t(ϕ) (u(ψ) z) (z

and commutation with all other constructs. (Since no recursive calls of t are made on ψ, its duplication does not lead to exponential blowup; recall that by the current assumption, the translation u of agent formulae does essentially nothing.) We thus obtain the following result.

Theorem 9 (Upper complexity bound). If the agent logic is a fragment of the full µ-calculus, then the satisfiability problem of AGEL is in EXPTIME.

Proof sketch. We need to show that the translation t is really satisfiability-equivalent. From a model M, x0 of an AGEL formula ϕ, with M = (X, A, VW, ), we construct a model (M , x0) of t(ϕ), with M = (X , R, V ), as follows. Following the intention of the translation t(ϕ) as indicated above, we take X to be the union of the set X of worlds, the set Ag of agents (the underlying set of A), and the set Ag X of (agent, world) pairs, assuming w.l.o.g. that these sets are disjoint. We interpret the syntactic material (atomic programs and atomic propositions) mentioned in agent formulae in ϕ over Ag X like in the given agent model A, exploiting that the agent logic is a fragment of the full µ-calculus. Similarly, we interpret world atoms on X in the same way as in M. Finally, we interpret π1, π2 as the expected projections R(π1) = {((a, x), a) | (a, x) Ag X}, R(π2) = {((a, x), x) | (a, x) Ag X}, and edge as

R(edge) = {(x, (a, y)) | x a y in M}.

It is not hard to see that (M , x) is really a model of ϕ. In the converse direction, given a model (M, x0) of the µ-calculus formula t(ϕ), with M = (X, R, V ), we construct a model (M , x0) of ϕ, with M = (X, A, VW, ), as follows. We use the original set X of worlds also as the underlying set Ag of the agent model A, whose structure we then obtain by just suitably restricting M. Similarly, we take VW to be the restriction of V to world atoms, i.e. we interpret world atoms in M like in M. Finally, as indicated above, we define the indistinguishability relation a for a Ag = X as the symmetric closure of the relation

{(x, y) | (x, e) R(edge). (e, a) R(π1), (e, y) R(π2)}.

Again, it is not hard to check that (M, x) is really a model of ϕ.

In combination with Theorem 6, we thus have

Corollary 10 (Complexity of AGEL). If the agent logic is a fragment of the full µ-calculus, then the satisfiability problem of AGEL is EXPTIME-complete.

Remark 11. Indeed the above encoding implies that one can raise the expressiveness of the agent logic to extensions of the full µ-calculus that remain decidable in EXPTIME. One candidate is the full hybrid µ-calculus (Sattler and Vardi 2001), which extends the full µ-calculus with nominals, i.e. propositional atoms denoting single objects. This opens the possibility of combining explicitly named agents in the standard sense with abstract groups of agents, as in the formula

CJohn has Friend.John Pub on Wednesdays,

which says that John and his friends know that their regular pub night is on Wednesdays.

Completeness and Bounded Models

We axiomatize AGEL in Hilbert style using the following system C5 of axioms and rules:

(T) Cψϕ ϕ ( ) ϕ C ϕ (K) Cψ(ϕ γ) (Cψϕ Cψγ) (4) Cψϕ CψCψϕ (5) Cψϕ Cψ Cψϕ (Ind) Cψ χ(ϕ (Cψϕ Cχϕ)) (ϕ Cψ χϕ)

(Nec) ϕ Cψϕ (AM ) γ ψ Cψϕ Cγϕ

Recall that by our running assumptions, the agent logic LAg is closed under all propositional connectives. We write C5 ϕ if an AGEL formula ϕ is derivable in this system; ϕ is consistent if C5 ϕ. For a finite set Γ of formulae, we write bΓ for the conjunction of all formulae in Γ, and we say that Γ is consistent if bΓ is consistent. The system includes the usual S5 axioms for common knowledge, reflecting normality (axiom (K)), reflexivity (axiom (T)), transitivity (axiom (4)), and Euclideanity (axiom (5)), as well as the usual necessitation rule (Nec). As usual, the (K) axiom implies commutation of Cψ with conjunction, and hence, together with the necessitation rule (Nec), monotonicity and replacement of equivalents for Cψ. Specific properties of AGEL are reflected in the axiom ( ), which, together with (T), says that C ϕ holds almost vacuously, in the sense that it does not claim any agent to know anything but requires ϕ to be true in the current world; in the rule (AM ), which says that Cψϕ is antimonotone in ψ, as requiring fewer agents to know ϕ is a weaker claim; and, centrally, in the induction axiom (Ind), which captures the fact that the indistinguishability relation A B for a union A B of two sets A, B of agents is the reflexive-transitive closure of the union of the indistinguishability relations A, B for the original sets. The rule (AM ) implies replacement of equivalents in the index of Cψ (from equivalence of ψ and ψ , derive equivalence of Cψϕ and Cψ ϕ). Via (AM ), the system depends on reasoning in the agent logic, which we will assume to be completely axiomatized. We note first that the induction axiom generalizes to multiple disjuncts:

Lemma 12. Every formula of the form

CWn i=1 ψi(ϕ (Vn i=1 Cψiϕ)) (ϕ CWn i=1 ψiϕ)

(for n 0) is derivable in C5.

We explicitly record soundness of the system:

Theorem 13 (Soundness). If C5 ϕ then |= ϕ.

We show completeness via a finite canonical model construction that is related to the standard treatment of propositional dynamic logic (PDL) in that it needs to close canonical models under transitivity (Fischer and Ladner 1979; Blackburn, de Rijke, and Venema 2001). This construction requires some restrictions on the agent logic:

Definition 14. We say that the agent logic LAg has the filtered model property if, for each finite set ΣAg of agent formulae that is closed under subformulae, there is an agent model A(ΣAg), with underlying set denoted by Ag(ΣAg), such that on the one hand any two distinct agents in Ag(ΣAg) are distinguished by a formula in ΣAg (in particular Ag(ΣAg) is finite, namely at most exponential in |ΣAg|), and on the other hand for every satisfiable subset Γ ΣAg, there is an agent in Ag(ΣAg) that satisfies all formulae in Γ. Since the agent logic is closed under propositional connectives, we then have, for each agent a Ag(ΣAg), a characteristic agent formula ba (a propositional combination of ΣAgformulae) such that Jba KA(ΣAg) = {a}. We put

Clo Ag(ΣAg) = ΣAg {ba | a Ag(ΣAg)}.

Example 15. As indicated in the introduction, ALC has the filtered model property (and is completely axiomatized), and in fact one can go beyond ALC to some degree. In particular, the extension of ALC with nominals, ALCO, still has the filtered model property. (See also comments in Remark 11.) We fix from now on a consistent AGEL formula ρ0. We base our canonical model construction on a suitable notion of closure. Definition 16 (Normalized negation). We let ϕ = χ if ϕ has the form ϕ = χ, and ϕ = ϕ otherwise. Definition 17 (Closure). Let ΣAg be the closure of the set of agent formulae occurring in ρ0 under taking subformulae. Then the closure Σ of ρ0 is the least set of world formulae containing ρ0 that is closed under (world) subformulae and normalized negation, and moreover satisfies

if Cχϕ Σ and ψ Clo Ag(ΣAg), then Cψϕ Σ

(with Clo Ag(ΣAg) as per Definition 14). We next construct a weak form of model of ρ0 that assigns indistinguishability relations to sets of agents without regard to their definition via reflexive-transitive closure; this will be rectified in a subsequent step. Definition 18 (Pseudo-model). An AGEL pseudo-model Mp = (X, A, VW, p) consists of a set X of worlds, an agent model A with underlying set Ag of agents, a valuation VW: At W P(X) of the world atoms, and an equivalence relation p A on X for each subset A Ag. The semantics of AGEL over pseudo-models is defined like over models, except that the interpretation of Cψ uses the relation p JψKA in place of JψKA.

We construct a canonical pseudo-model Cp Σ = (XΣ, A(ΣAg), VW, p) by taking XΣ to consist of the maximal consistent subsets of Σ; A(ΣAg) as per Definition 14; VW(p) = {Γ XΣ | p Γ}; and

Γ p JψKA bΓ Pψ consistent

where by Pψ we denote the dual of Cψ, i.e. Pψϕ := Cψ ψ. Well-definedness is guaranteed by the properties of A(ΣAg); indeed we shall often write p ψ in place of p JψKA for readability, similarly for . We note that Σ inherits exponential size from Clo Ag(ΣAg), so XΣ is of doubly exponential size in the size of ρ0.

Lemma 19. The relations p ψ are reflexive and symmetric.

The point of using the canonical pseudo-model is that it allows for a straightforward proof of the usual existence lemma:

Lemma 20 (Existence Lemma). Let Γ XΣ be a world in the canonical pseudo-model Cp Σ such that Cψϕ Γ. Then there exists XΣ such that Γ p ψ and ϕ

Leveraging characteristic agent formulae, we can derive a proper AGEL-model, the canonical model CΣ, from the canonical pseudo-model Cp Σ by taking

where we exploit that by Remark 3, we do not need to care whether a is transitive. The key point is then that the existence lemma survives this transition thanks to the following fact, which hinges on the induction axiom (Ind):

Lemma 21. For all formulae ψ Clo Ag(ΣAg), p ψ JψKA

It is then straightforward to establish the expected truth lemma, making use of the fact that Clo Ag(ΣAg) contains all requisite characteristic agent-formulae:

Lemma 22 (Truth Lemma). Let Γ be a world in the canonical model CΣ. Then for all ϕ Σ,

ϕ Γ CΣ, Γ |= ϕ.

Completeness and the bounded model property are then immediate:

Corollary 23 (Completeness over finite models). Suppose that LAg has the filtered model property and is completely axiomatized. Then C5, together with the axiomatization of LAg, is weakly complete, i.e. every valid AGEL formula is derivable. Moreover, AGEL has the bounded model property: if a formula ρ0 is satisfiable, then ρ0 has a finite model with at most doubly exponentially many worlds in the size of ρ0.

Conclusions

We have introduced abstract-group epistemic logic (AGEL), a logic for reasoning about the common knowledge of groups of agents that are described abstractly via defining properties. We have established EXPTIME-completeness, a bounded model property, and (necessarily weak) completeness of a natural axiomatization. The EXPTIME upper bound holds in spite of the fact that the expected encoding into standard group epistemic logic (with a common knowledge operator for enumerated groups of agents) incurs exponential blowup, and relies instead on a satisfiability-preserving translation into the µ-calculus with converse. Key directions for future research concern in particular extensions of the logic by a distributed knowledge operator; by dynamic epistemic modalities such as public announcements; by expressive means for describing groups of agents via their individual knowledge; and by allowing non-rigid agent names and agent atoms to capture knowledge about agents.

Acknowledgements

This work was supported by DFG (German Research Foundation) as part of the Research Training Group 2475 Cybercrime and Forensic Computing (grant number 393541319/GRK2475/1-2019) and the project RAND: Reconstructing Arguments from Newsworthy Debates (grant number 377333057). The authors also wish to thank the anonymous reviewers for their suggestions and feedback.

Baader, F.; Calvanese, D.; Mc Guinness, D.; Nardi, D.; and Patel-Schneider, P., eds. 2003. The Description Logic Handbook. Cambridge University Press. ISBN 0-521-78176-0. Baltag, A.; Moss, L. S.; and Solecki, S. 1998. The Logic of Public Announcements and Common Knowledge and Private Suspicions. In Gilboa, I., ed., Theoretical Aspects of Rationality and Knowledge, TARK-1998, 43 56. Morgan Kaufmann. B ılkov a, M.; Christoff, Z.; and Roy, O. 2021. Revisiting Epistemic Logic with Names. In Theoretical Aspects of Rationality and Knowledge, TARK 2021, volume 335 of EPTCS, 39 54. Blackburn, P.; de Rijke, M.; and Venema, Y. 2001. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. de Rijke, M. 1993. Extending Modal Logic. Ph.D. thesis, Universiteit van Amsterdam Institute for Logic, Language and Computation. Fagin, R.; Halpern, J. Y.; Moses, Y.; and Vardi, M. Y. 1995. Reasoning About Knowledge. MIT Press. ISBN 9780262562003. Fischer, M. J.; and Ladner, R. E. 1979. Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci., 18(2): 194 211. Fitting, M.; Thalmann, L.; and Voronkov, A. 2001. Term Modal Logics. Stud Logica, 69(1): 133 169. Grove, A. J. 1995. Naming and Identity in Epistemic Logic Part II: A First-Order Logic for Naming. Artif. Intell., 74(2): 311 350. Grove, A. J.; and Halpern, J. Y. 1993. Naming and Identity in Epistemic Logics Part I: The Propositional Case. J. Log. Comput., 3(4): 345 378. Humml, M.; and Schr oder, L. 2022. Common Knowledge of Abstract Groups. Co RR, abs/2211.16284. Huth, M.; and Ryan, M. D. 2004. Logic in Computer Science - Modelling and Reasoning about Systems (2. ed.). Cambridge University Press. ISBN 9780511264016. Lutz, C. 2006. Complexity and succinctness of public announcement logic. In Autonomous Agents and Multiagent Systems, AAMAS 2006, 137 143. ACM. Mares, E. 2020. Relevance Logic. In The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Winter 2020 edition.

Moses, Y.; and Tuttle, M. 1988. Programming Simultaneous Actions Using Common Knowledge. Algorithmica, 3: 121 169. Naumov, P.; and Tao, J. 2019. Everyone Knows that someone Knows: Quantifiers over Epistemic Agents. Rev. Symb. Log., 12(2): 255 270. Padmanabha, A.; and Ramanujam, R. 2019. Two variable fragment of Term Modal Logic. In Mathematical Foundations of Computer Science, MFCS 2019, volume 138 of LIPIcs, 30:1 30:14. Schloss Dagstuhl Leibniz-Zentrum f ur Informatik. Pavlovic, D. 2021. Probabilistic Annotations for Protocol Models. In Dougherty, D.; Meseguer, J.; M odersheim, S.; and Rowe, P., eds., Protocols, Strands, and Logic, volume 13066 of LNCS, 332 347. Springer. Sattler, U.; and Vardi, M. 2001. The Hybrid -Calculus. In Automated Reasoning, IJCAR 2001, volume 2083 of LNCS, 76 91. Springer. Streett, R. 1982. Propositional Dynamic Logic of Looping and Converse Is Elementarily Decidable. Inf. Control., 54(1/2): 121 141. Vardi, M. 1998. Reasoning about The Past with Two-Way Automata. In Automata, Languages and Programming, ICALP 1998, volume 1443 of LNCS, 628 641. Springer. Venema, Y. 1996. A Crash Course in Arrow Logic. In Arrow Logic and Multi-Modal Logic, Studies in Logic, Language, and Information. European Association of Logic, Language and Information (Fo LLI). ISBN 9781575869858.