Succinctness of Epistemic Languages

1 Introduction

In Knowledge Representation, one of the key issues is to design logical languages that are useful to reason about a given set of structures, or models. Prominent examples are firstorder languages to reason about structured domains, temporal languages to reason about time structures, and modal logics to reason about Kripke models. It may well be that two languages L1 and L2 are equally expressive on a set of models under consideration: any difference between two models can be expressed in L1 iff it can be expressed in L2. However, even if the two languages are equally expressive, L1 may be preferred over L2, if the two languages have the same computational complexity, but L1 is more succinct than L2: what one can say in both languages can be done shorter in L1 than in L2 (formal definition to follow). Let us abbreviate these three criteria to saying that L1 is strictly preferred over L2. In this paper we show for two epistemic languages, that they are strictly preferred over the 'standard epistemic language' [Fagin et al., 1995]. The first example is conceptually simple: in epistemic logic for m agents, rather than writing a conjunction K1ϕ∧K2ϕ∧ · · · ∧Kmϕ, one can introduce an operator E ('everybody knows'), where Eϕ is defined as this conjunction (this definition implies that there is no added expressivity, and equal complexity is established in [Lutz, 2006]). The E operator acts as an approximation for common knowledge (but without its computational complexity) in defining levels Petar Iliev Computer Science Univ. of Liverpool pvi@liverpool.ac.uk Barteld Kooi Univ. of Groningen Philosophy B.P.Kooi@rug.nl of consensus in policies and protocols in multi-agent systems. Our result is relevant for e.g., query languages: in epistemic logic, one can query a scenario ('who knows what?') more succinctly using the E operator.

The second language that we demonstrate to be strictly preferred over standard epistemic logic is that of Public Announcement Logic (PAL, [Plaza, 1989]). PAL enriches multiagent epistemic logic with a construct [ϕ]ψ: 'after the announcement of ϕ, formula ψ is true'. Surprisingly, the language of public announcements is equally expressive as that of multi-agent epistemic logic. However, as was proven in [Lutz, 2006], the language of public announcement logic is computationally equally complex as, but more succinct than that of epistemic logic. But the succinctness result was only proven under the general, weak semantics Km of modal logic. An issue left as an open problem in [Lutz, 2006, p. 140] is whether public announcement logic is also more succinct than epistemic logic under the semantics S5m: Kripke models where each relation is an equivalence relation, which is the class generally used for epistemic logics. One of the results in our paper is that we settle this question positively: the result holds also under S5m.

Although the paper focuses on the two epistemic languages described, we hope our techniques are applicable to various modal languages. Let us briefly explain why succinctness may fail when moving to a stronger semantics. To say that L1 is more succinct than L2 under semantics S roughly means that there are formulas ϕ1, ϕ2, . . . in L1 such that any formulas ψ1, ψ2, . . . in L2 that are equivalent to them in S must be significantly longer. In a stronger semantics S ′ there are generally more formulas that are equivalent to ϕi than in S. So, under S ′ , we may find more candidates ψi in L2 that are equivalent to ϕi, and some of themmight be shorter than those found under S.

How to demonstrate that a formula equivalent to ψ ∈ L2 must have at least a certain length? We propose to use Formula Size Games (FSGs), introduced in [Adler and Immerman, 2003]: which establish a direct link between the number of moves needed for one player to win, and the size of formulas associated with the game. Hence, reasoning about the shortest formulas equivalent to ψ amounts to reasoning about the shortest strategies to win an FSG related to ψ. In our formulation, FSG's, become essentially one-player games, which makes it easier to reason about winning strategies.

2 Preliminaries

In this paper, for each m ∈ N we fix a set of agents Ag = {a1, . . . am} and atoms At = {p1, p2, . . . }.

Definition 1 (Formulas) The formulas ψ of the language of public announcement logic LPAL are :

where p ∈ At and a ∈ Ag. We denote the language not containing any formula of the form [ψ1]ψ2 or Eψ with LEL, the language of basic epistemic logic. The language not containing any formula of the form [ψ1]ψ2 is denoted LELE.

For a modal operator X and n ∈ N, the formula Xnϕ is defined as usual: X0ϕ = ϕ and Xn+1ϕ = XnXϕ. The length of a formula |ψ| is defined in the obvious way (note that we do not count parentheses): |⊥| = |⊤| = |p| = 1, |ψ1∧ψ2| = |ψ1∨ψ2| = |ψ1|+|ψ2|+1 and |¬ψ| = |Kaψ| = |Maψ| = |Eψ| = 1 + |ψ|, |[ψ1]ψ2| = |ψ1| + |ψ2|.

Definition 2 (Kripke Model) AKripkemodel forAg andAt is a tuple 〈S,R, V 〉 where S is a set of states, R : Ag → P(S×S), for which we write sRat rather than (s, t) ∈ R(a), and V : P → 2S determines for every p ∈ P the set of states V (p) ⊆ S where p is true.

Given a model M = 〈S, R, V 〉, a pointed model is a pair (M, s) (sometimes written M, s) where s ∈ S. We will also write such a pair as M, s. Sets of pointed models are denoted M,M′ ,M1,M2, . . . .

Definition 3 (Satisfaction) M, s |= ϕ is defined as usual: we only give the modal clauses:

M, s |=Maϕ iff for some v, sRav andM, v |= ϕ; M, s |=Kaϕ iff for all v, sRav implies M, v |= ϕ; M, s |= [ϕ]ψ iff if M, s |= ϕ, thenM|ϕ, s |= ψ.

where M|ϕ is the submodel of M restricted to the set of worlds where ϕ is true. We define

The fact that the operator E is defined using the operator K shows that LELE and LEL are equally expressive. Using the reduction axioms below (cf. [Plaza, 1989]), one proves that LPAL and LEL are equally expressive, too.

Definition 4 (Formula Size Game) The formula size game (FSG) between Spoiler and Duplicator is played on a tree, where each node is labeled with a pair 〈M ◦ M′ 〉 such that M and M′ are sets of pointed models. At each step of the game, a node gets labeled with one of the symbols from the set S = At ∪ {⊤,⊥, ¬, ∨, ∧} ∪ {Ma,Ka | a ∈ Ag} and either it is closed or at most two new nodes are added. Given a node 〈M ◦ M′ 〉, Spoiler can make the following moves at this node:

• ⊥-move This can be played only if M = ∅. When Spoiler plays this move, the leaf 〈M◦M′ 〉 is closed and labeled with the symbol ⊥.
• ⊤-move This can be played only if M′ = ∅. When Spoiler plays this move, the node is closed and labeled with the symbol ⊤.
• atomic-move Spoiler chooses a propositional variable p such that every pointed model in M satisfies p, and no pointed model in M′ does. After this move, this node is closed and labeled with the symbol p.

not-move Spoiler labels the node with the symbol ¬ and adds one new node labeled 〈M′ ◦M〉 as a successor to the node 〈M ◦ M′ 〉.

• and-move Spoiler labels the node with the symbol ∧ and splits M′ in two (not necessarily disjoint) sets M′ = M′ 1 ∪ M′ 2. Two new nodes are added to the tree as successors to 〈M◦M′ 〉, namely 〈M◦M′1 〉 and 〈M◦M′2 〉.
• or-move Spoiler labels the node with the symbol ∨ and splits M in two (not necessarily disjoint) sets M = M1 ∪ M2. Two new nodes are added to the tree as successors to the node 〈M◦M′ 〉, namely 〈M1 ◦M′ 〉 and 〈M2 ◦M′ 〉.
• Ka-move Spoiler initiates this move by labeling the node with Ka and, for each pointed model (M ′ ,w′ ) ∈ M′ he chooses a pointed model (M ′ , v′ ) such that w′R′a v′ . Then, Duplicator responds by choosing for each pointed model (M,w) ∈ M all the possible pointed models (M, v) such that wRav. If for some (M,w) w does not have an Ra successor, Duplicator chooses no (M, v) for the pointed model (M, w). A new node consisting of the sets of pointed models that the players have chosen is added as a successor to the node 〈M◦M′ 〉.
• Ma-move Spoiler labels the node with the symbol Ma and for each pointed model (M,w) ∈ M, he chooses a pointed model (M, v) such that wRav. Duplicator responds by choosing for each pointed model (M ′ ,w′ ) ∈ M′ all the possible pointed models (M ′ , v′ ) such that w′R′a v′ . If for some (M ′ ,w′ ) w′ does not have an R′a successor, Duplicator chooses no (M ′ , v′ ) for the pointed model (M ′ ,w′ ). A new node consisting of the sets of pointed models that the players have chosen is added as a successor to the node 〈M◦M′ 〉.

and-moves and or-moves are collectively called splitting moves. Ma-moves and Ka-moves are called agent moves. The game is defined by specifiying a top-node 〈M ◦ M′ 〉.

FSG's were first introduced in [Adler and Immerman, 2003] for first-order logic with two variables and the transitive closure operator for CTL. We added the and-move, ⊤- move and ⊥-move. Moreover, our Ma-move is the modal translation of their EX-move, for which we also cater for the possibility that a world has no successors (and our Kamove is a dual of it). However, in a direct translation of the EX-move to our Ma-move, the response of Duplicator would have prescribed that she chooses for every M ′ ,w′ ∈ M′ some (rather than all) possible models M ′ , v′ ∈ M′ such that w′Rav′ . Our formulation models a 'strongest' strategy of Duplicator: she wins the game using our strategy iff she has a winning strategy in the game as defined in [Adler and Immerman, 2003]. So, our formulation makes the game essentially a one-player game, in which Duplicator is not left with any choice during the game- our formulation plays her optimal strategy.

Definition 5 Given a game tree T with n nodes that is the result of an FSG, we say that Spoiler has won the game in n moves iff every leaf of T is closed. Otherwise Duplicator has won.

The next theorem connects FSGs with the length of formulas in the language of basic epistemic logic LEL.

Theorem 1 Spoiler can win the FSG starting with 〈M ◦ M′ 〉 in n moves iff there is a formula ϕ in LEL of size n true in all models of M but false in all of M′ .

Proof (If) Suppose that there is a formula ϕ of size n such that every pointed model in M satisfies ϕ and no pointed model in M′ does. We prove by induction on the structure of ϕ that Spoiler can win the game starting in 〈M ◦ M′ 〉 in n moves by playing according to ϕ.

Base case: If ϕ is the formula ⊥, and every model in M satisfies ϕ, it is obvious that M = ∅ and Spoiler can win the game by playing a ⊥-move. Similarly for ⊤. If ϕ is the propositional variable p, then Spoiler plays the atomic-move and the tree is closed, as required. It is obvious that the tree has just one node, i.e. Spoiler can win the game in |ϕ| moves by playing according to ϕ.

Induction step: We only present the step for the Ka-move. If ϕ is a formula of the form Kaψ, then for each model (M ′ ,w′ ) ∈ M′ Spoiler chooses a model (M ′ , v′ ) such that w′R′a v′ and ψ is false in (M ′ , v′ ). Let N′ be the set of models Spoiler has chosen. For each pointed model (M, w) ∈ M, Duplicator chooses all the possible pointed models (M, v) such that wRav. Let N be the set of models Duplicator has chosen. A new node 〈N ◦ N′ 〉 is added as a successor of 〈M ◦ M′ 〉. Clearly, ψ must be true in all the new pointed models Duplicator has chosen and false in all of those that Spoiler has chosen. Applying the induction hypothesis, we see that Spoiler can win the subgame starting at 〈N ◦ N′ 〉 in |ψ| moves. Therefore, Spoiler can win the FSG starting at 〈M ◦ M′ 〉 in |ϕ| = |Kaψ| = |ψ| + 1 = n moves by playing according to ϕ.

(Only if) Suppose that Spoiler has won the n-round formula size game starting at 〈M◦M′ 〉. We claim that the game tree is a parse tree of a formula of length n that is true in all the models in M and false in all the models in M′ . In order to prove this, we label the nodes of the tree step by step starting with the leaves. These were labeled during the game with the propositional variables p, ⊤ and ⊥ that Spoiler used to close them. Then the rest of the nodes are labeled successively. If a node has a ¬ label and its successor is labeled with ψ, then that node is labeled with ¬ψ, etc. By a straightforward backward induction on the tree we can see that for each node we have the following.

• The string of symbols labeling the node is indeed a wellformed formula of the language LEL.
• The formula labeling the node is true in all the models on the left and false in all the models on the right. There-

fore, the formula labeling the root of the tree is true in all the pointed models in M and false in all the pointed models inM′ .

It is obvious that the game tree is a parse tree for the formula labeling the root. □

Definition 6 (Succinctness) Let L1 and L2 be two logical languages and let S be a class of models (or 'semantics'). We say that L1 is exponentially more succinct than L2 on S, and we write L1 ≺S L2, if there exists a sequence of formulas ϕ0, ϕ1, . . . in L1 such that

1. for every n, |ϕn+1| > |ϕn|, and
2. there is a polynomial f > 0 of degree at least 1 such that for every sequence ψ0, ψ1, · · · ∈ L2 with ψn ≡S ϕn, for all n, we have |ψn| ≥ 2f(|ϕn|) .

Note that it is possible to have both L1 ≺S L2 and L2 ≺S L1 at the same time. However, if L1 ⊆ L2, we can only have L2 ≺S L1.

Proposition 1 Let S and T , be two classes of models such that S ⊆ T and let L1, L2 be two languages. If L1 ≺S L2, then L1 ≺T L2.

Our strategy to prove that L1 ≺ L2 under semantics S consists of defining an infinite sequence of formulas ϕ0, ϕ1, . . . , in L1 such that:

1. for some d, for every n > 0, |ϕn+1| = |ϕn| +d;
2. for every n, we construct two sets of pointedmodelsMn and M′n from S such that ϕn is true in all Mn, but false in all of M′n , and the number of moves for Spoiler to win the game starting in 〈Mn ◦M′n 〉 is at least 2n .

Lemma 1 If L1 and L2 are such that there is a sequence of formulas ϕ0, ϕ1, . . . in L1 satisfying the two requirements above, then L1 ≺ L2 under S.

In this paper, L2 = LEL. In Section 3, L1 = LELE, and in Section 4, L1 = LPAL. In Section 3.1, the semantics is Km, and in Sections 3.2 and 4, the semantics is S5m.

3 Succinctness of LELE

In this section we prove that LELE is exponentially more succinct than LEL on the class of S5m models. However, we first look at the simpler case for the semantics Km.

3.1 Succinctness of LELE on K2

Let the formulas ϕn ∈ LELE be:

If we define ψ0 = p and ψn+1 = Maψn ∨Mbψn, It is obvious that ϕn ∈ LELE is equivalent to ψn ∈ LELE. Formula ϕn expresses that there is some p-world at most n steps away.

We now define two sets of pointed models Mn and M′n for each n whose underlying frame is a binary tree of depth n. The vertices of the tree are labelled with a and b and the nodes are labeled with words over {a, b}. M′n contains only one model: the binary tree of depth nwith no atom true anywhere. Mn consists of all the models based on binary trees of depth n containing just one world satisfying the proposition p and this world is a leaf.

Definition 7 (Words) For a set of Ag we define the set of words of length at most n, Wn(Ag) as follows. W0 = {ϵ} and Wn+1 = Wn ∪{wx | w ∈ Wn & x ∈ Ag}. The length of w and concatenation of words is defined in the standard way. For a word w, w1 denotes its first component, w2 its second, etc. If Ag is clear, we will writeWn rather thanWn(Ag). For k ∈ N with k ≥ |Ag|, let W ̸=k n (Ag) ⊆ Wn(Ag) be the set of k-diff words, that is, words w for which every subsequence of length k is such that all elements in that subsequence are different.

Definition 8 (K2-models for E) For each n > 0 and each w ∈ Wn({a, b}), we define a model M n w = 〈W, R, V 〉, where

• W = Wn is as defined earlier;
• V (p) = {w}
• Riuv iff v = ui (i ∈ {a, b}).

Let Mn consist of all the models M n w , ϵ. Furthermore, M′n contains the binary tree (Bn , ϵ) with Bn = 〈Wn,R, V 〉 where V (p) = ∅. Let us say that (M n w , v) is a-imperfect if the p world can only be reached from v by first taking a step along the relation Ra. Similarly for b-imperfect models.

It is clear that every model in Mn satisfies ϕn, while the only model in M′n falsifies ϕn. Therefore, Spoiler can win the game starting at 〈M⋉ ◦ M′n 〉.

Lemma 2 Fix n ∈ N. Consider the FSG game with initial node 〈Mn ◦ M′n 〉 and suppose Spoiler plays a winning strategy. Then, in the tree generated by the play, for every different words x and y over Ag, there are two different closed branches.

Proof First note that in any node of the game tree, the state of all pointed models will be at the same distance from ϵ. For the first n agent-moves that Spoiler plays, and for α = a, b, the effect of an Mα-move and that of a Kα-move are the same (since at depth ≤ n, every model has exactly one a and one bsuccessor). Since the only state where M n w , ϵ and Bn , ϵ differ in an atom is at state w, Spoiler needs to reach state w in both models. As long as there are an a-imperfect and a b-imperfect model on the same side of the node, Spoiler cannot play an agent-move, since in one of the models it would lead to a successor from which only ¬p worlds are reachable (which is also the case in the model Bn on the other side of the node, implying that Spoiler would lose the game). But this proves the lemma: if x ̸= y, at some point in the game one of the models M n x and M n y will be a-imperfect while the other is b-imperfect. □

Theorem 2 On K2, the language LELE is exponentially more succinct than LEL.

Proof Note that |ϕn| = n + 3. Now let ψn be an arbitrary formula in LEL that is equivalent to ϕn. Spoiler is able to win the FSG starting in 〈Mn ◦M′n 〉 as defined above, but any such game has a distinct branch for any word w ∈ Wn(Ag). There are at least 2n such branches. By Theorem 1, ψn is at least 2n long. □

The proof of Theorem 2 also shows that on the class of binary trees, LELE is exponentially more succinct than LEL and that LELE is exponentially more succinct than LEL for any Km with m ≥ 2.

3.2 Succinctness of LELE in S5m

Modal logics for knowledge typically assume some additional properties of the K-operator. In particular, it is often assumed that knowledge is veridical (for all ϕ, we have Kaϕ → ϕ), and that agents have positive (Kaϕ → KaKaϕ) and negative (¬Kaϕ → Ka¬Kaϕ) introspection. The semantics S5m is obtained by requiring that in a model M = 〈S,RAg, V 〉, the accessibility relations Ra are equivalence relations. Inspecting the proof of Lemma 2, it is not difficult to see that building a similar proof for S5m is harder: in the proof of Lemma 2 we for instance relied on the fact that once Spoiler takes an Ma-move in a model that is b-imperfect, the p-world can never be reached again. In S5m, such an argument is not valid, because Spoiler and Duplicator can always go back to the initial state after playing an Ma-move, or a Ka-move. We will see that in order to cater for this, our models in this section will be a bit more involved than those in the previous section, and moreover, we present our result only for the case in which m ≥ 4: we come back to this in Remark 1.

However, for games on S5m models, we may assume that Spoiler never plays two moves in succession that involve the same agent. One way to see this is to first recall [Meyer and van der Hoek, 1995] the following equivalences as validities of S5m, where a is an arbitrary agent:

This can even be strengthened to the following equivalences in S5m, where we assume that Xa, Ya ∈ {Ka,Ma} and ◦ ∈ {∧, ∨} (cf. [Meyer and van der Hoek, 1995, Section 1.7.6]:

Definition 9 (Simple S5m-strategies) A strategy is a simple S5m-strategy for Spoiler if for any path in the game tree, two consecutive agent-moves (even when separated by moves different from agent-moves) concern different agents.

Lemma 3 (Simple S5m-strategies Lemma) Let M and M′ be sets of pointed S5m models. If Spoiler can win the FSG starting in 〈M ◦ M′ 〉 and the resulting closed game tree contains n nodes and b branches, then he can also win this FSG using a simple S5m-strategy, resulting in a game tree with at most n nodes and at most b branches.

Definition 10 (S5m-models for E) Let m ≥ 3. Given n ∈ N and 3-diff word w of length n, the model M n w = 〈S,R, V 〉 is determined as follows (see also Figure 1, left):

Note that fromM n w , u0 there is a path of length n ('down', in Figure 1, left), following the agents in w, to the only pworld, un. The shortest path from v0 to a p-world takes n+1 steps. The states ui and ui+1 are connected through agent wi+1, similarly for vi and vi+1. Also, ui and vi are connected through agent a iff there is no other a-arrow leaving ui or vi: neither 'up' (through wi) nor 'down' (through wi+1). Finally, for fixed n, let Mn be the set of models M n w , u0 and let M′n be the set of models of the formM n w , v0, where w ranges over all 3-diff words over Ag.

Observation 1 Define ϕn again as in (1). It is easy to check that ϕn is true in Mn and false in M′n , and hence he can win the game starting in 〈Mn ◦ M′n 〉. Consider two models M n , u0 and M n , v0 appearing at node η = 〈Mn ◦ M′n 〉.

w

w

1. In order to win the game, Spoiler needs to reach states that disagree on an atom, i.e., he has to reach the models M n , un and M n , vn

w

w

1. If in some node M n w , ui and M n w , vi appear, no matter what Spoiler's play is, there will be a branch such that in the next node M n w , uj and M n w , vj both appear (j ∈ {i - 1, i, i + 1}
2. If in some node M n w , ui and M n w , vi appear and Spoiler is going to play an agent a-move, then (1) if i = 0, a has to be w + 1, (2) if 0 < i < n, a has to be wi-1 or wi, and (3) if i = n, a has to be wn. This is because in all other cases, ui and vi have the same a-successors, so that Duplicator's response in that case would lead to a node where some model appears on both sides of the node, which is a loss for Spoiler. In the case of (3), if the last agent-move was an wn-move, if Spoiler plays a simple S5m-strategy, no agent moves will be played any further.

Lemma 4 Let n be given. Consider the game starting in node η = 〈Mn ◦ M′n 〉, and suppose Spoiler plays a winning simple S5m-strategy. Then, in the tree generated by the play, for every two different 3-diff words x and y over Ag, there are two different closed branches.

Proof By Observation 1, items 1 and 2, from η, at some point Spoiler has to play an agent-move. By Observation 1.3, this implies that if x1 ̸= y1, in order to play an agentmove, Spoiler has to first split the node such that M n x , u0 and M n y , u0 appear at different nodes, which gives rise to two different branches. If x1 = y1, Spoiler can play an agent x1-move, generating a node which includes the models M n x , u1 and M n , y, u1 on one side of the node, and the models M n x , v1 and M n y , v1 on the other. We can repeat this argument, Spoiler playing some splitting moves and notmoves, and some agent xi+1 = yi+1-moves visiting nodes with models M n x , ui andM n y , ui on one side of the node, and the models M n x , vi and M n y , vi on the other side, until either xi+1 ̸= yi+1, (reaching a node where Spoiler has to create the two branches we were looking for), or reaching a node where xi+1 = yi+1 but where Spoiler decides to play 'down' in one model, say M n x but stays at the 'same level' with M n y . Thus, the resulting node of such a move would contain M n x , zi+1 and M n y , zi on one side of the node, and M n x , ri+1 andM n y , ri on the other for some z ̸= r ∈ {u, v}. .

If i + 1 = n, by Observation 1.3, no agent-moves need to be played for M n x , zi+1, while still some have to be played for M n y , zi, so Spoiler will need to create two separate branches. If i + 1 ̸= n, for M n x , zi+1, Spoiler's next agent-move is an xi+2-move, and for M n y , zi, it needs to be an yi-move. Since xi+2 ̸= xi = yi, Spoiler needs to first separate the M n x , zi+1 models from the M n , zi models. □

y

Theorem 3 (Succinctness of Everybody Knows in S5m) For m ≥ 4, LELE ≺S5m LEL.

Proof Note that |ϕn| = n + 3. Any closed game tree with root 〈Mn ◦ M′n 〉 contains a different branch for every w ∈ W ̸=3 n (Ag). There are at least (m- 2)n such different paths. So if m ≥ 4, we apply Lemma 1. □

Corollary 1 In any system weaker than S5m (m ≥ 4), LELE ≺S5m LEL.

Remark 1 The proof of Lemma 4 would not hold if we had not restricted our words to be 3-diff word. To see this, consider the two different paths x = ababcab and y = abcabab. Spoiler might well be playing agent-moves in the order ababcabab in a node where the models M 7 x , u0 and M 7 y , u0 both appear in the starting node: instead of having two different branches, this would generate one (slightly longer) branch that leads to a closing node. Now, for |Ag| =m= 2, there are only two 3-diff words, and if m = 3, there are only 6 such words. Only when m ≥ 4, the number of 3-words grows exponentially. Obviously, Theorem 3 does not hold for m = 1, which leaves us the open problem whether it holds for m = 2, 3.

4 Public Announcement Logic

For LPAL, in our presentation we will assume to have at least 6 agents, we will later argue this can be brought down to 4.

For any n ∈ N, let 2|n denote that n is even. In the sequel assume that Ag = O ∪ E, with O = {o1, o2, o3} and E = {e1, e2, e3}. We will also use O ∪ E as our set of atomic propositions. Define, for a set A ⊆ Ag the formula

Definition 11 Consider the following sequence of formulas ϕn ∈ LPAL, n ∈ N.

Definition 12 Consider the following sequence of formulas ψn ∈ LEL, n ∈ N.

Lemma 5 For all n, S5m |= ϕn ↔ ψn.

The models M n w , u0 and M n w , v0 that we will define will agree on the first conjunct of ψn, but they will disagree on the second conjunct (n > 1).

Definition 13 Define the set of coloured alternating words (ca-words) w over O and E of length n, notation Πn (O, E), or shortly Πn , as follows: (1) w ∈ W ̸=3 n , (2) for i < n : wi ∈ O ⇒ wi+1 ∈ E and wi ∈ E ⇒ wi+1 ∈ O and (3) w1 ∈ E if 2|n, w1 ∈ O else. So a ca-word w in Πn has no repetition of an agent in any sub-word of length 3, it alternates between agents from O and E and the first agent is from E iff n is even. If n is even, each model M n w is determined by an ca-word w of even length, otherwise w has an odd length. Model M n w = 〈S, R, V 〉 is constructed as follows (see Figure 1 (right) for a model M 3w ). Let A(a) = O if a ∈ O and A(a) = E if a ∈ E.

So, we have a state z0 in S, in which all the atoms are true. Moreover, no atom is true in u0, v0, and the states u0, v0 and z0 are all i-accessible from each other for all i ∈ Ag \A(w1), that is, if n is odd, all states u0, v0, z0 are E-accessible from each other, and if n is even, they are O-accessible.

The other states in M n w form again a ladder: we have states v1, v2, . . . , vn, u1, u2, . . . un in S and stipulate that atom p (p ∈ {oi, ei | 1 ≤ i ≤ 3}) is true in vi and ui (i < n) iff wi = p. The only state for which we make an exception is vn: here, no atom is true. In terms of access, we state that Rgvivi+1 iff Rguiui+1 iff wi+1 = g (i < n). Moreover, access between ui, ui+1, vi, vi+1 is defined as in Definition 10. The class of models M n , u0 thus obtained will be M(n) and the class of models M n w , v0 is denoted M′ (n).

Lemma 6 Let n ∈ N, w ∈ Πn , and ψn be as defined earlier. M n w , u0 |= ψn but M n w , v0 ̸|= ψn.

The following Lemma and Theorem are proven as in the previous section.

Lemma 7 Let n be given. Consider the game starting in node η = 〈Mn ◦ M′n 〉, and suppose Spoiler plays a winning simple S5m-strategy. Then, in the tree generated by the play, for every two different x and y from Πn , there are two different closed branches.

Theorem 4 (Succinctness of LPAL) For m ≥ 6, we have LP AL ≺S5m LEL.

Corollary 2 In any system weaker than S5m (m ≥ 6) the language LPAL is exponentially more succinct than LEL.

Consider four agents Ag = {a1, a2, b, c} and define ϕ0 = ⊤, ϕ3i+1 = 〈ϕi〉(Ma1 a1 ∨Ma2 a2), ϕ3i+2 = 〈ϕi〉Mbb, and ϕ3i+3 = 〈ϕi〉Mcc. Words are now built by gluing sequences a1bc and a2bc together, and Lemma 7 would go through in this setting, but this time, for n ∈ N, there will be 2n/3 different words, which is still sufficient to prove Theorem 4.

Proposition 2 For m ≥ 4, LPAL ≺S5m LELE.

5 Conclusion

We used FSGs to establish three succinctness results for epistemic logics under various semantics. It is interesting to explore what kind of assumptions about Spoiler's strategy one is allowed to make under other semantics. This could lead to a 'toolkit' for FSGs to be used for a suite of logics,.

Apart from settling the question of succinctness of LELE and LPAL for m = 3, future work would explore the use of FSGs for other logics, like for instance for Coalition Logic with its non-standard modal semantics. Finally, we'd like to make a precise connection between FSGs on the one hand, and other kind of games that are used in modal logics property checking or model checking, like games based on μ-calculus (cf. [Stirling, 1997]) or bisimulation games (where the emphasis is on modal depth rather than formula size).