Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games

Pfau, Sebastian

doi:10.4230/LIPIcs.CSL.2026.35

Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games

Sebastian Pfau

Technische Universität Ilmenau, Germany

Abstract

The Hella-Vilander game for modal logic is a model comparison game that captures the formula size necessary to separate sets of pointed Kripke structures. We introduce the $\mathcal{M}$ -ON game as a modification of this game. Our game captures the necessary number of modal operators, i.e., $\Diamond$ and $\Box$ instead of formula size. We use our game to show that the bi-implication $\leftrightarrow$ , sometimes also called equivalence, enables us to write modal logic formula with significantly fewer modal operators. With this we show, that with bi-implications we can also write significantly shorter modal logic formulas. This result holds even if only special classes of Kripke structures are considered. To be more precise we show that there is an exponential succinctness gap between modal logic and its extension with bi-implication on the class of structures with a transitive and reflexive accessibility relation, as well as on the class of structures with a symmetrical and reflexive accessibility relation. Lastly we show that for the class of structures with a transitive and symmetrical accessibility relation this succinctness gap disappears.

Keywords and phrases:

succinctness, modal logic, model comparison games

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics

DOI:

10.4230/LIPIcs.CSL.2026.35

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Model comparison games, like the Ehrenfeucht-Fraïssé game [4, 6], are a type of logic games. They can be used to prove that it is difficult to express certain properties in a logic. For example the game defined by Adler and Immerman in [1] has been used to prove lower bounds for formula size in FO²(TC) and the logic CTL. Extended syntax trees [8] can be seen as an equivalent method to this game, even though they drop the game setting. The game and the syntax tree method can also be modified to work on other logics, see [7, 12, 13] for examples. In [9] Hella and Vilander introduce their own game, which builds on the Adler-Immerman game. This Hella-Vilander game is defined for modal logic and the $\mu$ -calculus, but it can also be adapted for other logics. The main idea of this game is as follows: players $S$ (Spoiler, Samson) and $D$ (Duplicator, Delilah) play on two sets of structures $\mathbb{A}$ and $\mathbb{B}$ with a resource parameter $k$ . Player $S$ spends the parameter $k$ in order to make his moves, while $D$ answers. $S$ has to play a winning move before $k$ runs out. In such a play $S$ has a winning strategy if, and only if, there is a formula $\varphi$ of size at most $k$ of the corresponding logic, that separates $\mathbb{A}$ and $\mathbb{B}$ .

There are also model comparison games that only count the number of occurrences of specific characters, instead of the more general formula size. See [3, 5] for examples. As part of their conclusion Hella and Vilander suggest that their game can be modified to count a more specific parameter as well. One such possible parameter is the number of modal operators used, i.e., $\Diamond$ and $\Box$ . This can be done, because every move of the Hella-Vilander game corresponds to some character of a separating formula. So by simply adjusting the way the parameter $k$ has to be spend, we can create a game for the number of modal operators instead of formula size. The main problem with this approach is that some moves do not reduce the parameter at all. Firstly this opens up the possibility of endless games, where $S$ cannot win, but he can ensure he does not lose either. Secondly it makes the game inefficient, since moves that do not change the parameter are inherently less interesting.

In order to deal with these problems we look at another model-comparison game used by Vinall-Smeeth in [14]. He calls this game the $k$ -QVT game. However in this paper we use the parameter $k$ with a different meaning. So in order to avoid confusion we will use the name $l$ -QVT game when referring to this game instead. The $l$ -QVT counts the number of quantifiers in formulas of the $l$ -variable fragment of first-order logic. It can be seen as a modification of the Adler-Immerman game, where after every move all structures without a partially isomorphic counterpart in the respective other set are removed. This is possible, because these are exactly the structures that can be removed in the Adler-Immerman game without playing any quantifier-moves. With this idea we can create our own game, which counts the number of modal-operators of separating modal logic formulas. We call this game the $\mathcal{M}$ -Operator-Number game.

Afterwards we use our new game in order to look at how different sets of Boolean connectives can be used to write more succinct formulas. This topic was already researched by Berkholz, Kuske and Schwarz in [2]. They show that all complete operator sets, which only contain so-called locally monotone operators, have the same succinctness up to a polynomial. On the other hand all sets that contain some non locally monotone operator also coincide in succinctness. In this paper we use the De Morgan basis, consisting of $\land$ , $\lor$ and $\lnot$ , as a candidate from the first class and the De Morgan basis extended by the bi-implication $\leftrightarrow$ as a candidate of the second. Berkholz et al. also show that for modal logic there is an exponential succinctness gap between these two classes. They prove this by working directly with formulas and using intricate and ad hoc arguments. This gap still exists if only reflexive Kripke structures are taken into consideration. However if the focus is tightened even further to only Kripke structures with an equivalence relation as accessibility relation, then this succinctness gap is closed.

From these findings some interesting follow-up questions emerge: Is it possible to remove $\leftrightarrow$ without significantly increasing the number of modal operators? This question is interesting because modal logic formulas with few modal operators are easier to work with. However we answer this question negatively by showing that there is an exponential operator-succinctness gap between modal logic and modal logic with bi-implication as well. Another interesting follow-up question is the following: What about other classes of Kripke-structures? We want to answer this question in this paper. In particular we show that for the class of Kripke structures with a reflexive and transitive accessibility relation, as well as the class of structures with a reflexive and symmetrical relation this exponential succinctness gap exists. This directly implies that the gap also exists for the class of transitive and the class of symmetrical structures. For all of these classes there is an exponential operator-succinctness gap as well. Only for the class of structures with a transitive and symmetrical relation this gap disappears. In this way our work offers a more complete and systematic examination of the connection between succinctness and the basis of boolean connectives in modal logic on special classes of Kripke structures.

2 Preliminaries

2.1 Modal logic with Bi-implication and Kripke structures

Let $P$ be an infinite set of propositional variables, also called labels. We define ML $[\leftrightarrow]$ as the set of all modal logic formulas over $P$ using $\top$ and $\bot$ as constants, $\Diamond$ and $\Box$ as modal operators, as well as $\lnot$ , $\lor$ , $\land$ and $\leftrightarrow$ as Boolean connectives. Formally ML $[\leftrightarrow]$ is the set of all formulas generated by the following grammar:

\varphi::=\bot\mid\top\mid p\mid\lnot\varphi\mid(\varphi\lor\varphi)\mid(% \varphi\land\varphi)\mid(\varphi\leftrightarrow\varphi)\mid\Diamond\varphi\mid\Box\varphi

where $p\in P$ is a propositional variable. Now modal logic can be defined as a restriction of modal logic with bi-implication. So ML is defined as the set of all formulas from ML $[\leftrightarrow]$ that do not contain any occurrences of $\leftrightarrow$ .

Let $\mathcal{M}=(W,R,V)$ be a connected, directed, labelled graph, where $W$ is the set of possible worlds or nodes, $R\subseteq W\times W$ is a binary accessibility relation and $V:W\rightarrow\mathcal{P}(P)$ is a labelling function, assigning sets of propositional variables to each node. For a node $w\in W$ we call $V(w)\subseteq P$ the colour of $w$ . If $V(W):=\bigcup\limits_{w\in W}V(w)$ , the set of all labels used in $\mathcal{M}$ , is finite, we say $\mathcal{M}$ is a finitely labelled graph. The tuple $(\mathcal{M},w)$ is called a pointed Kripke structure or just Kripke structure. It should be noted here, that our naming conventions might differ from the norm. In the literature the labelled graph $\mathcal{M}$ is sometimes referred to as a Kripke structure, while $(\mathcal{M},w)$ is called a pointed Kripke structure. However in this paper we do not view $\mathcal{M}$ as a structure. Also our conventions allow us to use the terms pointed Kripke structure, Kripke structure or sometimes just structure interchangeably when referring to $(\mathcal{M},w)$ .

Let $A\subseteq W$ be a set of nodes. We write $(\mathcal{M},A)$ to mean the class of structures $\{(\mathcal{M},w)\mid w\in A\}$ . We define $\Box w=\{w^{\prime}\in W\mid(w,w^{\prime})\in R\}$ as the set of all successors of a node $w$ . This notation can also be extended to sets of nodes with $\Box A=\bigcup\limits_{w\in A}\Box w$ and structures with $\Box(\mathcal{M},w)=(\mathcal{M},\Box w)=\{(\mathcal{M},w^{\prime})\mid w^{% \prime}\in\Box w\}$ . The extension to classes of structures is defined in the obvious way. We can now start giving the definition of the semantics of modal logic with bi-implication on Kripke structures.

The satisfaction relation $\models$ is defined inductively as follows:

1.

$(\mathcal{M},w)\models\top$ and $(\mathcal{M},w)\not\models\bot$ for all $(\mathcal{M},w)$
2.

$(\mathcal{M},w)\models p$ iff $p\in V(w)$
3.

$(\mathcal{M},w)\models\lnot\varphi$ iff $(\mathcal{M},w)\not\models\varphi$
4.

$(\mathcal{M},w)\models(\varphi\lor\psi)$ iff $(\mathcal{M},w)\models\varphi$ or $(\mathcal{M},w)\models\psi$
5.

$(\mathcal{M},w)\models(\varphi\land\psi)$ iff $(\mathcal{M},w)\models\varphi$ and $(\mathcal{M},w)\models\psi$
6.

$(\mathcal{M},w)\models\varphi\leftrightarrow\psi$ iff $(\mathcal{M},w)\models(\varphi\land\psi)\lor(\lnot\varphi\land\lnot\psi)$
7.

$(\mathcal{M},w)\models\Diamond\varphi$ iff $(\mathcal{M},v)\models\varphi$ holds for some $v\in\Box w$
8.

$(\mathcal{M},w)\models\Box\varphi$ iff $(\mathcal{M},v)\models\varphi$ holds for all $v\in\Box w$

Next we extend this satisfaction relation to classes of structures. Let $\mathfrak{A}$ be a class of pointed Kripke structures. Then $\mathfrak{A}\models\varphi$ if, and only if, $(\mathcal{M},w)\models\varphi$ for all $(\mathcal{M},w)\in\mathfrak{A}$ . We say a formula $\varphi$ separates two classes of pointed Kripke structures $\mathfrak{A}$ and $\mathfrak{B}$ if either $\mathfrak{A}\models\varphi$ and $\mathfrak{B}\models\lnot\varphi$ , or $\mathfrak{B}\models\varphi$ and $\mathfrak{A}\models\lnot\varphi$ . So $\varphi$ must be true for all structures of one class and for no structure of the other class. In this case we will also call $\varphi$ a separating formula. It should be noted here that our definition differs slightly from the definition used by Hella and Vilander. In their definition $\varphi$ is a separating formula only if $\mathfrak{A}\models\varphi$ and $\mathfrak{B}\models\lnot\varphi$ . However it is easy to see that if $\varphi$ is a separating formula by our definition then $\varphi$ or $\lnot\varphi$ is a separating formula by their definition. For $\mathfrak{A}=\{\mathcal{A}\}$ and $\mathfrak{B}=\{\mathcal{B}\}$ we might also say $\varphi$ separates $\mathcal{A}$ and $\mathcal{B}$ instead of $\mathfrak{A}$ and $\mathfrak{B}$ .

We say that two formulas $\varphi$ and $\psi$ are equivalent, in writing $\varphi\equiv\psi$ , if every pointed Kripke structure $(\mathcal{M},w)$ satisfies $\varphi$ if, and only if, it satisfies $\psi$ . Let $\mathcal{C}$ be some class of Kripke structures. Then two formulas $\varphi$ and $\psi$ are equivalent on $\mathcal{C}$ , in writing $\varphi\equiv_{\mathcal{C}}\psi$ , if every pointed Kripke structure $(\mathcal{M},w)\in\mathcal{C}$ from $\mathcal{C}$ satisfies $\varphi$ if, and only if, it satisfies $\psi$ .

2.2 Formula size

The size of a formula $\varphi$ is the number of symbols needed to write it, excluding brackets. This can be expressed quite easily using the following inductive definition:

1.

$|\varphi|=1$ if $\varphi\in\{\top,\bot\}\cup P$
2.

$|\varphi|=|\psi|+1$ if $\varphi=\lnot\psi$ , $\varphi=\Diamond\psi$ or $\varphi=\Box\psi$
3.

$|\varphi|=|\psi|+|\chi|+1$ if $\varphi=\psi\land\chi$ , $\varphi=\psi\lor\chi$ or $\varphi=\psi\leftrightarrow\chi$

Similarly the operator-number of $\varphi$ is the number of modal operators, i.e. $\Diamond$ and $\Box$ , used in the formula. The inductive definition is as follows:

1.

$|\varphi|_{O}=0$ if $\varphi\in\{\top,\bot\}\cup P$
2.

$|\varphi|_{O}=|\psi|_{O}$ if $\varphi=\lnot\psi$
3.

$|\varphi|_{O}=|\psi|_{O}+1$ if $\varphi=\Diamond\psi$ or $\varphi=\Box\psi$
4.

$|\varphi|_{O}=|\psi|_{O}+|\chi|_{O}$ if $\varphi=\psi\land\chi$ , $\varphi=\psi\lor\chi$ , or $\varphi=\psi\leftrightarrow\chi$

The term succinctness is used to compare logics based on the length of formulas needed to express the same property. Given two logics $L_{1}$ , $L_{2}$ with the same expressiveness and a function $f:\mathbb{N}\rightarrow\mathbb{N}$ , we say $L_{1}$ is $f$ -times more succinct than $L_{2}$ if, and only if, for every $n\in\mathbb{N}$ there is a formula $\varphi\in L_{1}$ with $|\varphi|\geq n$ , so that $|\psi|\geq f(|\varphi|)$ for every $L_{2}$ -formula $\psi$ with $\psi\equiv\varphi$ . If $f$ is an exponential function, we also say $L_{1}$ is exponentially more succinct than $L_{2}$ . Let $\mathcal{C}$ be a class of structures, then succinctness on $\mathcal{C}$ is defined by taking the definition of succinctness and replacing $\equiv$ with $\equiv_{\mathcal{C}}$ .

Succinctness is based on formula size, but we can define a corresponding measurement for operator-number. We say that $L_{1}$ is $f$ -times more operator-succinct than $L_{2}$ if, and only if, for every $n\in\mathbb{N}$ there is a formula $\varphi\in L_{1}$ with $|\varphi|_{O}\geq n$ , so that $|\psi|_{O}\geq f(|\varphi|_{O})$ for every $L_{2}$ -formula $\psi$ with $\psi\equiv\varphi$ . Exponential operator-succinctness and operator-succinctness on special classes of structures are defined in the obvious way.

Counter intuitively it is theoretically possible that there are two logics $L_{1}$ and $L_{2}$ where $L_{1}$ is exponentially more succinct than $L_{2}$ and $L_{2}$ is exponentially more succinct than $L_{1}$ . This is because there might be some properties that can be expressed more succinctly in $L_{1}$ , while some other properties can be expressed more succinctly in $L_{2}$ . However this cannot happen for the logics examined in this paper. Since every ML formula is also an ML $[\leftrightarrow]$ formula, ML cannot be more succinct than ML $[\leftrightarrow]$ .

3 The operator-number game

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph and let $A,B\subseteq W$ be two sets of nodes of the graph. Then $\{A,B\}$ is an unordered pair. From this point on, we will use just the term pair to refer to unordered pairs. We say such a pair $\{A,B\}$ is tidy, if for every $a\in A$ there is a $b\in B$ with $V(a)=V(b)$ and vice versa. For any sets $A$ and $B$ , $\{A,B\}$ can be tidied up by removing all nodes $a\in A$ without a fitting node in $B$ and all $b\in B$ without a fitting node in $A$ . Let $t(\{A,B\})=\{A^{\prime},B^{\prime}\}$ , where $A^{\prime}\subseteq A$ and $B^{\prime}\subseteq B$ are the largest subsets of $A$ and $B$ respectively, so that $\{A^{\prime},B^{\prime}\}$ is tidy.

Definition 1.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $A_{0},B_{0}\subseteq W$ two sets of nodes and $k_{0}\in\mathbb{N}$ . The $\mathcal{M}$ -Operator-Number game, or $\mathcal{M}$ -ON game for short, played from $A_{0}$ and $B_{0}$ with parameter $k_{0}$ has two players $S$ and $D$ . An $S$ -position $(\{A,B\},k)$ of the game consists of a tidy pair of sets of nodes $A,B\subseteq W$ , as well as a parameter $k\in\mathbb{N}$ . The starting position is $(t(\{A_{0},B_{0}\}),k_{0})$ . A turn for $S$ starts from an $S$ -position and proceeds in one of the following two ways:

1.

Split-move: $S$ may only play this type of move if $k\geq 2$ . He picks a set $X\in\{A,B\}$ and splits it into two disjoint and non-empty sets $X_{1}$ and $X_{2}$ . Then he chooses two parameters $k_{1},k_{2}\geq 1$ with $k_{1}+k_{2}=k$ . Let $Y$ be the set that fulfils $\{X,Y\}=\{A,B\}$ . This play by $S$ creates the $D$ -position $(X_{1},X_{2},Y,k_{1},k_{2})$ . Afterwards $D$ plays by taking the set $Y$ and picking a subset $Y^{\prime}\subseteq Y$ of it. Then she chooses $i\in\{1,2\}$ and the game continues from the $S$ -position $(t(\{X_{i},Y^{\prime}\}),k_{i})$ .
2.

Operator-move: $S$ may only play this type of move if $k\geq 1$ . He picks a set $X\in\{A,B\}$ and then picks a function $f:X\rightarrow\Box X$ , where $f(x)\in\Box x$ for every $x\in X$ . Let $X^{\prime}=\{f(x)\mid x\in X\}$ be the image of $X$ under $f$ and let $Y$ be the set with $\{X,Y\}=\{A,B\}$ . Then the $D$ -position after this move by $S$ is $(X^{\prime},Y,k-1)$ . Afterwards $D$ plays by taking the set $Y$ and then determining a set $Y^{\prime}\subseteq\Box Y$ of successors of the nodes from $Y$ . The game continues from the position $(t(\{X^{\prime},Y^{\prime}\}),k-1)$ .

Player $S$ wins a play of the game, if the play arrives at a position $(\{A,B\},k)$ with $A=B=\emptyset$ . Otherwise if $S$ cannot make another move, player $D$ wins.

When looking at an operator-move we might say $S$ picks $x^{\prime}$ as a successor of $x$ instead of $S$ picks a function $f$ with $f(x)=x^{\prime}$ . We usually make $D$ play in such a way that no nodes are removed during tidy-up. For this reason we will only mention the tidy-up process if nodes are getting removed. The composition of a $D$ -position depends on the type of move played by $S$ . However in contrast to $S$ -positions we mainly view $D$ -positions as intermediate positions. So it is not necessary to give a full definition for them.

The parameter $k$ is reduced in every move and the play cannot continue, once the parameter is depleted. So a play with starting parameter $k$ can go on for $k$ rounds at most. In particular every play has to be finite. This implies in every play either player $S$ or player $D$ wins. So our game is a finite, chance-less two-player game with complete information, that cannot end in a draw. Then by Zermelo’s Theorem for every position of the $\mathcal{M}$ -ON game one of the players, $S$ or $D$ , has a positional winning strategy.

Such a positional strategy for a player, $S$ or $D$ , is a partial map $f_{S}$ or $f_{D}$ . For $S$ a strategy $f_{S}$ takes as input an $S$ -position and outputs a $D$ -position, that can be reached from the input position via a single move by $S$ . It is a winning strategy, if every play where $S$ plays according to $f_{S}$ is won by him. Similarly a strategy $f_{D}$ for $D$ takes a $D$ -position as input and gives an $S$ -position, reachable in one move by $D$ , as output. It is a winning strategy, if $D$ wins every play in which she plays $f_{D}$ . If player $S$ has a winning strategy for some position $(\{A,B\},k)$ , we will say this position is a winning position for player $S$ . The definition of winning positions for $D$ is done in the obvious way.

As previously stated, the main influence for our game is the Hella-Vilander game from [9], which in turn builds on the Adler-Immerman game from [1]. Before we show that our game can be used to prove lower bounds for operator-number, we want to discuss how our game differs from these games.

The $\mathcal{M}$ -ON game is played by two players, $S$ (Samson) and $D$ (Delilah), just like the game defined by Hella and Vilander. However instead of playing on two sets of structures, in our game the players play on unordered pairs of sets of nodes. This shows two significant differences between our game and their game. Firstly we are using nodes, where they used structures. This change however is only notational, because we will still implicitly talk about pointed Kripke structures. We will use the node $w$ as a representation of the structure $(\mathcal{M},w)$ . In order to do so, we have to fix a single graph $\mathcal{M}$ for the entire game. So every pointed Kripke structure that appears in a play must be based on the same labelled graph. While this appears like a real restriction, it is possible to merge multiple labelled graphs into one without changing the validity of formulas at any world.

The second significant difference is that we use unordered pairs instead of ordered pairs or tuples. This change allows us to switch around the elements of our pairs at will. In the game by Adler and Immerman, such a switch is used as a not-move. So basically in our game, we can simulate a not-move without actually making a move. This is possible, because we are only interested in the number of operators and not in the number of negations. We also add an additional step to every move, where we tidy up the pair of our position. By doing so we remove all elements, that could have been removed in the Hella-Vilander game by $S$ playing a number of turns without playing an operator-move. A similar approach is used in the $l$ -QVT game from [14]. In this game structures without a partially isomorphic counterpart in the other set are removed after every step. A problem with this method occurs when tidying up would skip an infinite number of moves. Vinall-Smeeth solves this problem by only considering finite structures. However for our purposes a weaker condition is sufficient. We only demand that our graphs are finitely labelled.

As a last major difference: In the Hella-Villander game, player $D$ is forced to play following the so-called oblivious strategy. This means she always has to answer with the largest possible set. This works, because this oblivious strategy is always optimal. So if $D$ can win the game, she can do so by playing obliviously. While this simplifies the definition of the game, it would also complicate our proofs. Simply put we only want to prove that $D$ has a winning strategy. Whether this strategy is also optimal is of no importance to us. Sometimes $D$ playing in a suboptimal way might lead to smaller positions, which can simplify our proofs.

Our aim is to prove that the $\mathcal{M}$ -ON game can be used to characterize the number of operators needed in order to separate sets of nodes. As a stepping stone towards this goal, we state the following two lemmas.

Lemma 2.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph and $A,B,A^{\prime},B^{\prime}\subseteq W$ be sets of nodes with $t(\{A,B\})=\{A^{\prime},B^{\prime}\}$ . If there is a separating formula $\varphi^{\prime}$ for $(\mathcal{M},A^{\prime})$ and $(\mathcal{M},B^{\prime})$ , then there is also a separating formula $\varphi$ for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|_{O}=|\varphi^{\prime}|_{O}$ .

Lemma 3.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $A,B\subseteq W$ be sets of nodes that form a tidy pair and let $\varphi$ be an ML-formula without any modal operators. Then $(\mathcal{M},A)\models\varphi$ if, and only if, $(\mathcal{M},B)\models\varphi$ .

Now we want to prove the following Correctness- and Completeness-Theorem for our game. We do so by proving both directions separately, beginning with the proof of correctness.

Lemma 4.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $A,B\subseteq W$ two sets of nodes and $k\in\mathbb{N}$ . If $S$ has a winning strategy in the $\mathcal{M}$ -ON game played from $A$ and $B$ with parameter $k$ , then there is an ML-formula $\varphi$ separating $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|_{O}\leq k$ .

Proof.

For this proof we assume that $S$ has a winning strategy for the $\mathcal{M}$ -ON game played from $A$ and $B$ with parameter $k$ . Because of Lemma 2 we may assume that $A$ and $B$ already form a tidy pair. Then the starting position of this game is $(\{A,B\},k)$ . We construct the separating formula $\varphi$ by induction over $k$ . First we look at the base case $k=0$ . Since the parameter is already used up, $S$ cannot make a move at all. So the only possible way for him to win is, if the current position already fulfils $\{A,B\}=\{\emptyset,\emptyset\}$ . Then $\varphi=\top$ is a trivial separating formula.

We now assume, the implication holds for all parameters $k\leq i$ and we look at some winning strategy $f_{S}$ for the $\mathcal{M}$ -ON game starting from $(\{A,B\},i+1)$ . We have to differentiate between the types of moves $f_{S}$ prescribes as the next move from this position.

We begin by assuming that $f_{S}$ prescribes a split-move. In this case $S$ picks a set from $\{A,B\}$ , without loss of generality he picks $A$ . Then $S$ splits it into two sets $A_{1}$ and $A_{2}$ and he splits $i+1$ into $k_{1}$ and $k_{2}$ , both of which have to be at most $i$ . Since $f_{S}$ is a winning strategy for $S$ , it has to win against every possible strategy of $D$ , in particular against the following ones: $D$ answers by picking $B^{\prime}=B$ and then picks either $1$ or $2$ . The game continues from $(t(\{A_{1},B\}),k_{1})$ or $(t(\{A_{2},B\}),k_{2})$ respectively. From both positions $f_{S}$ is still a winning strategy. So thanks to our induction hypothesis and Lemma 2, for $j\in\{1,2\}$ we have separating formulas $\varphi_{j}$ for $(\mathcal{M},A_{j})$ and $(\mathcal{M},B)$ with $|\varphi_{j}|_{O}\leq k_{j}$ . We may assume $(\mathcal{M},A_{j})\models\varphi_{j}$ , because otherwise we could use $\lnot\varphi_{j}$ instead. Then $\varphi=\varphi_{1}\lor\varphi_{2}$ is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|_{O}=|\varphi_{1}|_{O}+|\varphi_{2}|_{O}\leq k_{1}+k_{2}=i+1$ .

Next we look into $f_{S}$ prescribing an operator-move. Once again we may assume that $S$ plays on $A$ . For every node in $A$ he picks a successor and forms $A^{\prime}$ . The strategy $f_{S}$ has to win against a strategy of $D$ that simply picks $B^{\prime}=\Box B$ . So $S$ can also win from the position $(t(\{A^{\prime},\Box B\}),i)$ . This means there has to be a formula $\varphi^{\prime}$ with $(\mathcal{M},A^{\prime})\models\varphi^{\prime}$ , $(\mathcal{M},\Box B)\models\lnot\varphi^{\prime}$ and $|\varphi^{\prime}|_{O}\leq i$ . So every node in $A$ has at least one successor, namely those picked by $S$ during the construction of $A^{\prime}$ , that satisfies $\varphi^{\prime}$ . On the other hand no node in $B$ can have such a successor, since all of them are part of $\Box B$ . So $\varphi=\Diamond\varphi^{\prime}$ is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with at most $i+1$ operators. This finishes our prove of the first implication. $\hfill\blacktriangleleft$

Next we prove the completeness of our game.

Lemma 5.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $\varphi$ an ML-formula, $A,B\subseteq W$ two sets of nodes and $k\in\mathbb{N}$ , so that $\varphi$ is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|_{O}\leq k$ . Then $S$ has a winning strategy in the $\mathcal{M}$ -ON game played from $A$ and $B$ with parameter $k$ .

Proof.

To begin with we may assume that the separating formula $\varphi$ only contains the connectives $\lor$ and $\lnot$ , as well as the operator $\Diamond$ , since otherwise we can use the well known equivalences $\psi\land\chi\equiv\lnot(\lnot\psi\lor\lnot\chi)$ and $\Box\psi\equiv\lnot\Diamond\lnot\psi$ in order to remove all occurrences of $\land$ and $\Box$ . None of these changes increase the number of modal operators, so $|\varphi|_{O}\leq k$ still holds. The $\mathcal{M}$ -ON game played from $A$ and $B$ with parameter $k$ has the starting position $(t(\{A,B\}),k)$ . If $\varphi$ is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ , it is also a separating formula for the tidied up subsets of $A$ and $B$ . So we may assume that $\{A,B\}$ is already tidy, meaning $t(\{A,B\})=\{A,B\}$ . We construct $f_{S}$ , the winning strategy of $S$ , by playing according to $\varphi$ . This construction is done by induction over the formula size of $\varphi$ .

For the base case, we look at all atomic formulas, so $\varphi\in P\cup\{\top,\bot\}$ . Because of Lemma 3, $(\mathcal{M},A)$ and $(\mathcal{M},B)$ agree on $\varphi$ . So the only way for $\varphi$ to be a separating formula is $A=B=\emptyset$ . In this case $(\{A,B\},k)$ is already a winning $S$ -position and $S$ does not have to make a move in order to win the play.

We now assume the implication holds for all formulas $\psi$ with $|\psi|\leq i$ and we look at a separating formula $\varphi$ for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|=i+1$ and $|\varphi|_{O}\leq k$ . We have to differentiate based on the outermost operator of $\varphi$ .

We begin with $\varphi=\lnot\psi$ . Because of our definition of separating formula, $\psi$ also is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\psi|=i$ and $|\psi|_{O}\leq k$ . So thanks to our induction hypothesis, $S$ already has a winning strategy for the $\mathcal{M}$ -ON game played on $A$ and $B$ with parameter $k$ .

Next we look at $\varphi=\Diamond\psi$ with $|\psi|=i$ and $|\psi|_{O}\leq k-1$ . This also implies $k\geq 1$ . So every node in one of the sets, w.l.o.g. we assume $A$ , has a successor that satisfies $\psi$ , while no node in the other set, $B$ , has such a successor. Then $f_{S}$ prescribes an operator-move, where $S$ picks for every $a\in A$ a successor $a^{\prime}$ with $(\mathcal{M},a^{\prime})\models\psi$ and collects them into the set $A^{\prime}$ . Then $D$ answers by gathering some nodes $b^{\prime}\in\Box B$ into a set $B^{\prime}$ . However none of the nodes picked by $D$ can satisfy $\psi$ . The game continues from the position $(t(\{A^{\prime},B^{\prime}\}),k-1)$ , where $\psi$ is a separating formula for $A^{\prime}$ and $B^{\prime}$ and thus also for the sets after tidying. So because of our induction hypothesis, for every choice made by $D$ during this turn, $S$ has a winning strategy from the resulting position. So $f_{S}$ simply copies the fitting strategy for $D$ ’s choice of $B^{\prime}$ .

For $\varphi=\psi\lor\chi$ we have to make an additional differentiation. It is possible that one of the sub-formulas, w.l.o.g. we assume $\chi$ , does not contain any modal operators. Then one of the sets, we assume $A$ , satisfies $\psi\lor\chi$ , while the other satisfies its negation, so $(\mathcal{M},B)\models\lnot\psi\land\lnot\chi$ . This implies $(\mathcal{M},B)\models\lnot\psi$ and $(\mathcal{M},B)\models\lnot\chi$ . So because of Lemma 3, we also know $(\mathcal{M},A)\models\lnot\chi$ , which in turn implies $(\mathcal{M},A)\models\psi$ . This means $\psi$ is also a separating formula for $A$ and $B$ with $|\psi|\leq i$ and $|\psi|_{O}\leq k$ . So our hypothesis offers a winning strategy for $S$ in $(\{A,B\},k)$ .

Lastly we look at $\varphi=\psi\lor\chi$ , where both $\psi$ and $\chi$ contain at least one modal operator. This implies $k\geq 2$ . Once again we assume $(\mathcal{M},A)\models\psi\lor\chi$ and thus $(\mathcal{M},B)\models\lnot\psi\land\lnot\chi$ . Let $A_{1}$ and $A_{2}$ be the disjoint subsets of $A$ with $A_{1}:=\{a\in A\mid(\mathcal{M},a)\models\psi\}$ and $A_{2}:=\{a\in A\mid(\mathcal{M},a)\models\lnot\psi\land\chi\}=A\setminus A_{1}$ . If one of these sets, w.l.o.g. we assume $A_{2}$ , is empty, then $A=A_{1}$ and thus $(\mathcal{M},A)\models\psi$ holds. So $\psi$ is a shorter separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ and according to our induction hypothesis $S$ has a winning strategy for the position $(\{A,B\},k)$ . Otherwise we know $A_{1}\neq\emptyset$ and $A_{2}\neq\emptyset$ . So $S$ may play a split-move where he splits $A$ into $A_{1}$ and $A_{2}$ . Then he picks the new parameters as $k_{1}=|\psi|_{O}$ and $k_{2}=k-k_{1}$ , which implies $k_{2}\geq|\chi|_{O}$ . Player $D$ answers by picking a set $B^{\prime}\subseteq B$ . Independent from her choice $(\mathcal{M},B^{\prime})\models\lnot\psi\land\lnot\chi$ holds. The game continues from either $(t(\{A_{1},B^{\prime}\}),k_{1})$ or $(t(\{A_{2},B^{\prime}\}),k_{2})$ . For the first case, $S$ can use $\psi$ as a separating formula for $A_{1}$ and $B^{\prime}$ . Similarly $\chi$ is a separating formula for $A_{2}$ and $B^{\prime}$ . So by our induction hypothesis every possible follow-up position is a winning position for $S$ and thus $(\{A,B\},k)$ is as well. $\hfill\blacktriangleleft$

Lemma 4 and Lemma 5 can be combined into the following Correctness- and Completeness-Theorem.

Theorem 6.

Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $A,B\subseteq W$ two sets of nodes and $k\in\mathbb{N}$ . Then $S$ has a winning strategy in the $\mathcal{M}$ -ON game played from $A$ and $B$ with parameter $k$ if, and only if, there is an ML-formula $\varphi$ with $|\varphi|_{O}\leq k$ , that is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ .

4 Succinctness between ML[ $\leftrightarrow$ ] and ML

We begin this section by proving some simple upper bounds for succinctness.

Lemma 7.

The logic ML $[\leftrightarrow]$ is at most exponentially more succinct and at most exponentially more operator-succinct than ML.

Proof.

It is quite easy to see that the succinctness gap between ML and ML $[\leftrightarrow]$ is at most exponential. We can simply replace every sub-formula $\varphi\leftrightarrow\psi$ with $(\varphi\land\psi)\lor(\lnot\varphi\land\lnot\psi)$ . Every time this is done, the formula size is doubled at most. Since the number of bi-implications cannot exceed the formula size, this procedure leads to an exponential size increase at worst.

However this method cannot provide an upper bound for the operator-succinctness. While every such substitution only doubles the numbers of operators as well, we cannot bound the number of operators in the resulting formula by some function of the number of operators in the original formula. E.g. for a formula $\varphi$ with only one modal operator that appears in the scope of $n$ nested bi-implications this method would result in a formula with $2^{n}$ modal operators.

However there is another method, that guarantees an at most exponential increase in operator-number. This method is based on the construction used by Spira in [11]. We can use the equivalence $\alpha(\Diamond\beta)\equiv(\alpha(\top)\land\Diamond\beta)\lor(\alpha(\bot)% \land\lnot\Diamond\beta)$ , which holds as long as $\Diamond\beta$ does not appear in $\alpha$ in the scope of any operator. This allows us to inductively move all modal operators outside of the scope of any bi-implication. Every time this is done, the number of modal operators is doubled, which leads to an exponential increase. Then the bi-implications can be removed in the known way without increasing the number of modal operators any further. A more in-depth proof of this is given as part of the appendix. $\hfill\blacktriangleleft$

In the following Section 4.1 we show that there is an exponential succinctness gap between ML and ML $[\leftrightarrow]$ on the class of Kripke structures with a transitive and reflexive accessibility relation. Afterwards in Section 4.2 we show that this exponential succinctness gap also exists on the class of Kripke structures with a symmetrical and reflexive accessibility relation. Since these two claims are proven in similar ways, we want to use this opportunity to give a general overview of these proofs.

To begin with we construct an infinite graph $\mathcal{M}$ as well as two series of nodes $(a_{n})_{n\in\mathbb{N}}$ and $(b_{n})_{n\in\mathbb{N}}$ . Then for every $n\in\mathbb{N}$ we give an ML $[\leftrightarrow]$ -formula $\varphi_{n}$ . This formula separates $(\mathcal{M},a_{n})$ and $(\mathcal{M},b_{n})$ . The number of modal operators in $\varphi_{n}$ is bound from above by a polynomial over $n$ . Then we give some parameter $k_{n}$ that is exponential in $n$ and show that $(\{\{a_{n}\},\{b_{n}\}\},k_{n})$ is a winning position for player $D$ in the $\mathcal{M}-ON$ game. It follows that $S$ cannot have a winning strategy for this position. So by Theorem 6, there cannot be an ML-formula $\psi$ that separates $(\mathcal{M},a_{n})$ from $(\mathcal{M},b_{n})$ with $|\psi|_{O}\leq k_{n}$ implying that every ML-formula equivalent to $\varphi_{n}$ must be of size exponential in $n$ at least. This proves an exponential succinctness gap between ML and ML $[\leftrightarrow]$ for all classes of Kripke structures $\mathcal{M}$ belongs to.

Now we construct the infinite labelled graph $\mathcal{M}=(W,R,V)$ , which will be the basis for all of our other graphs. The nodes of this graph are formally defined as $W:=\{a_{0},b_{0}\}\cup\bigcup\limits_{i\geq 1}\{a_{i},b_{i},1_{i},2_{i},3_{i},% 4_{i},5_{i},6_{i},7_{i},8_{i},9_{i}\}$ . The edges of this graph are as follows:

R=\bigcup\limits_{i\geq 1}\left\{\begin{array}[]{l}(a_{i},1_{i}),(a_{i},2_{i})% ,(a_{i},3_{i}),(b_{i},1_{i}),(b_{i},3_{i}),(1_{i},4_{i}),(1_{i},6_{i}),(2_{i},% 4_{i}),(2_{i},7_{i}),(3_{i},5_{i}),\\ (3_{i},7_{i}),(4_{i},8_{i}),(4_{i},a_{i-1}),(5_{i},8_{i}),(5_{i},b_{i-1}),(6_{% i},a_{i-1}),(6_{i},9_{i}),(7_{i},b_{i-1}),(7_{i},9_{i})\end{array}\right\}

The graph $\mathcal{M}$ can be separated into segments. Then segment $i$ contains all nodes with index $i$ , as well as $a_{i-1}$ and $b_{i-1}$ . So the latter two nodes are shared nodes between segment $i$ and segment $i-1$ . The nodes and edges of segment $i$ are presented graphically in Figure 1. All edges of $\mathcal{M}$ connect nodes within a segment and all segments have equivalent edges. So this figure fully represents the nodes and edges of $\mathcal{M}$ . The numbers on the left side of the figure count the layers of the graph. Segment $i$ contains all nodes of layers $3i-1$ , $3i-2$ and $3(i-1)$ , as well as the nodes $a_{i}$ and $b_{i}$ from layer $3i$ . Lastly we define the labelling function of $\mathcal{M}$ . The labels we use are $\{p_{0},p_{1},q_{0},q_{1},q_{2}\}\subseteq P$ . The only node labelled with $p_{0}$ is $a_{0}$ . For every $i\geq 1$ the node $8_{i}$ is the only node of segment $i$ labelled with $p_{1}$ . Lastly we use the remaining labels $q_{0}$ , $q_{1}$ and $q_{2}$ in order to label the layers of the graph in an alternating pattern. More precisely for every $i\in\mathbb{N}$ we label all nodes of layer $3i$ with $q_{0}$ , all nodes of layer $3i-1$ with $q_{1}$ and all nodes of layer $3i-2$ with $q_{2}$ . The formal definition of the labelling function is given by the following list:

$\blacksquare$

$V(9_{i})=V(b_{i-1})=\{q_{0}\}$ for all $i\geq 1$ ,
$\blacksquare$

$V(8_{i})=\{p_{1},q_{0}\}$ for all $i\geq 1$ and
$\blacksquare$

$V(a_{i-1})=\begin{cases}\{p_{0},q_{0}\}&\text{for }i=1\\ \{q_{0}\}&\text{for all }i>1\end{cases}$
$\blacksquare$

$V(1_{i})=V(2_{i})=V(3_{i})=\{q_{1}\}$ for all $i\geq 1$ ,
$\blacksquare$

$V(4_{i})=V(5_{i})=V(6_{i})=V(7_{i})=\{q_{2}\}$ for all $i\geq 1$ ,

Figure 1: The

i

th segment of

\mathcal{M}

including labels.

Claim 8.

Let $\varphi_{i}$ be the ML formula inductively defined by $\varphi_{0}:=p_{0}$ and $\varphi_{i}:=\Diamond\Box((\Diamond p_{1})\leftrightarrow(\Diamond\varphi_{i-1% }))$ . Then $\varphi_{i}$ is a separating formula for $(\mathcal{M},a_{i})$ and $(\mathcal{M},b_{i})$ with $(\mathcal{M},a_{i})\models\varphi_{i}$ for every $i\in\mathbb{N}$ .

Proof.

This proof is done via induction on $i$ . For the base case $i=0$ the formula $\varphi_{i}=p_{0}$ holds only in $(\mathcal{M},a_{0})$ , because $a_{0}$ is the only node labelled with $p_{0}$ . Next let $i\geq 1$ be some positive number. We assume that our claim holds for $i-1$ . So $(\mathcal{M},a_{i-1})\models\varphi_{i-1}$ and $(\mathcal{M},b_{i-1})\models\lnot\varphi_{i-1}$ . Now we look at the other nodes of segment $i$ . We know $(\mathcal{M},8_{i})\models p_{1}$ , while no other node of layer $3(i-1)$ is labelled with $p_{1}$ . This implies $(\mathcal{M},4_{i})\models(\Diamond p_{1})\land(\Diamond\varphi_{i-1})$ , $(\mathcal{M},5_{i})\models(\Diamond p_{1})\land\lnot(\Diamond\varphi_{i-1})$ , $(\mathcal{M},6_{i})\models\lnot(\Diamond p_{1})\land(\Diamond\varphi_{i-1})$ , as well as $(\mathcal{M},7_{i})\models\lnot(\Diamond p_{1})\land\lnot(\Diamond\varphi_{i-1})$ . So $(\mathcal{M},4_{i})$ and $(\mathcal{M},7_{i})$ model $(\Diamond p_{1})\leftrightarrow(\Diamond\varphi_{i-1})$ , while $(\mathcal{M},5_{i})$ and $(\mathcal{M},6_{i})$ do not. Because $4_{i}$ and $7_{i}$ are the only successors of $2_{i}$ , this also means $(\mathcal{M},2_{i})\models\Box((\Diamond p_{1})\leftrightarrow(\Diamond\varphi% _{i-1}))$ . On the other hand, $1_{i}$ is a predecessor of $6_{i}$ and $3_{i}$ is a predecessor of $5_{i}$ . So neither $(\mathcal{M},1_{i})$ nor $(\mathcal{M},3_{i})$ satisfy this formula. Lastly $2_{i}$ is a successor of $a_{i}$ , so $(\mathcal{M},a_{i})\models\Diamond\Box((\Diamond p_{1})\leftrightarrow(% \Diamond\varphi_{i-1}))=\varphi_{i}$ . But $1_{i}$ and $3_{i}$ are the only successors of $b_{i}$ , so $(\mathcal{M},b_{i})\models\lnot\varphi_{i}$ , which proves the claim. $\hfill\vartriangleleft$

It should be noted here that the formula $\varphi_{i}$ does not contain any occurrences of either $q_{0}$ , $q_{1}$ or $q_{2}$ . However we need those labels in order to adapt $\varphi_{i}$ to the modified graphs we use in the following proofs.

4.1 Transitive and reflexive graphs

The graph $\mathcal{M}_{t,r}=(W,R_{t,r},V)$ is defined as an extension of $\mathcal{M}=(W,R,V)$ . The nodes and labels stay the same. First we add a self-loop for every node. So $(x,x)$ is a new edge for every node $x$ . Then we add a new edge from a node $x$ to a node $y$ , for all $x$ and $y$ where $x$ is a node on layer $i$ and $y$ is a node on layer $j$ with $i\geq j+2$ . So every node is now a predecessor to all nodes two or more layers below. So formally $R_{t,r}=R\cup\{(x,x)\mid x\in W\}\cup\{(x,y)\mid x\text{ belongs to layer $i$,% $y$ belongs to layer $j$, }i\geq j+2\}$ . It is easy to see that $\mathcal{M}_{t,r}$ is a reflexive graph. On top of that it is also transitive. Let $(x,y)$ and $(y,z)$ be edges of the graph. If either of them is a self loop, then $(x,z)$ is the same as the other edge. Otherwise $y$ must be on a lower layer than $x$ and $z$ must be on a lower layer than $y$ . So $z$ is at least two layers below $x$ and $(x,z)$ is an edge in $\mathcal{M}_{t,r}$ .

Lemma 9.

There are two polynomial functions $g_{1},g_{2}\colon\mathbb{N}\rightarrow\mathbb{N}$ , so that for every $n\in\mathbb{N}$ there is an ML $[\leftrightarrow]$ -formula $\psi_{n}$ , which separates $(\mathcal{M}_{t,r},a_{n})$ from $(\mathcal{M}_{t,r},b_{n})$ , with $|\psi_{n}|_{O}=g_{1}(n)\geq n$ and $|\psi_{n}|=g_{2}(n)\geq n$ .

Proof.

This is proven, by simply adapting the formula $\varphi_{n}$ from Claim 8 to separate $a_{n}$ and $b_{n}$ in $\mathcal{M}_{t,r}$ instead of in $\mathcal{M}$ . In $\mathcal{M}$ every edge goes down exactly one layer. But all edges added to $R$ when constructing $R_{t,r}$ go down at least two layers or are self-loops. So we need a way to determine what layer a node belongs to. We look at the formula $\chi_{i}^{+}$ defined by $\chi_{0}^{+}:=\top$ and $\chi_{i+1}^{+}:=\Diamond(q_{j}\land\chi_{i}^{+})$ with $i\in\mathbb{N}$ and $j=i\mod 3$ . This formula states, that there is a path of length $i$ that starts at the current node and on this path the labels $q_{0}$ , $q_{1}$ and $q_{2}$ appear in an alternating pattern. Such a path cannot use any self-loops, so every edge has to move down at least one layer. Then only nodes of layer $i$ or above satisfy this formula. Similarly only nodes of layer $i$ or below satisfy $\chi_{i}^{-}:=\lnot\chi_{i+1}^{+}$ . Now we can use the formula $\chi_{i}:=\chi_{i}^{+}\land\chi_{i}^{-}$ in order to check whether or not a node belongs to layer $i$ .

Then for any node $w$ of layer $i\geq 1$ $(\mathcal{M},w)\models\Diamond(\chi_{i-1}\land\varphi)$ holds if, and only if, $w$ has a successor exactly one layer below that satisfies $\varphi$ . Similarly $(\mathcal{M},w)\models\Box(\lnot\chi_{i-1}\lor\varphi)$ holds if, and only if, every successor of $w$ that is exactly one layer below the current layer satisfies $\varphi$ . So we can add conditions like these to $\varphi_{n}$ in order to only consider edges that go down exactly one layer, which are all edges from $R$ , while ignoring all edges from $R_{t,r}\setminus R$ . We define $\psi_{n}$ inductively with $\psi_{0}:=p_{0}$ and $\psi_{i}:=\Diamond(\chi_{3i-1}\land\Box(\lnot\chi_{3i-2}\lor((\Diamond(p_{1}% \land\chi_{3(i-1)})\leftrightarrow(\Diamond(\psi_{i-1}\land\chi_{3(i-1)})))))$ . Then for all nodes $w$ of layer $3n$ , $(\mathcal{M}_{t,r},w)\models\psi_{n}$ holds if, and only if $(\mathcal{M},w)\models\varphi_{n}$ . So by Claim 8, $\psi_{n}$ is a separating formula for $(\mathcal{M}_{t,r},a_{n})$ and $(\mathcal{M}_{t,r},b_{n})$ . For a rough estimation of the size of $\varphi_{n}$ we can assert that the number of times a sub-formula $\chi_{i}$ occurs in $\varphi_{n}$ is linear in $n$ . Also the size of such a formula is linear in $i$ , which is bounded from above by $3n-1$ . So the overall size of $\varphi_{n}$ is quadratic in $n$ , which is polynomial. A more in-depth examination leads to the findings $|\varphi_{n}|_{O}=24\cdot n^{2}+10\cdot n=:g_{1}(n)$ and $|\varphi_{n}|=36\cdot n^{2}+17\cdot n+1=:g_{2}(n)$ . $\hfill\blacktriangleleft$

Lemma 10.

There is an exponential function $h:\mathbb{N}\rightarrow\mathbb{N}$ , so that for every $n\in\mathbb{N}$ and for every ML-formula $\chi_{n}$ which separates $(\mathcal{M}_{t,r},a_{n})$ from $(\mathcal{M}_{t,r},b_{n})$ , we have $|\chi_{n}|_{O}>h(n)$ .

Proof.

First we define $h(n)=2^{n}-2$ . It is easy to see that $|\chi_{0}|_{O}>-1=h(0)$ holds. So from now on we may assume $n\geq 1$ . Then we show that there is no separating ML-formula for $\{(\mathcal{M}_{t,r},a_{n})\}$ and $\{(\mathcal{M}_{t,r},b_{n})\}$ with at most $h(n)$ modal operators. This is done by playing the $\mathcal{M}_{t,r}$ -ON game on $\{a_{n}\}$ and $\{b_{n}\}$ with parameter $h(n)$ and showing that $D$ has a winning strategy $f_{D}$ for these games. In order to do so we define the following sets of positions of the game.

$\blacksquare$

$W_{D}^{0}:=\bigl\{(\{A,B\},k)\mid A,B\subseteq W,A\cap B\neq\emptyset,k\in% \mathbb{N}\bigr\}$
$\blacksquare$

$W_{D}^{1}:=\bigl\{(\{\{a_{i}\},\{b_{i}\}\},k)\mid i\geq 1,k\leq 2^{i}-2\bigr\}$
$\blacksquare$

$W_{D}^{2}:=\bigl\{(\{\{2_{i}\},\{1_{i},3_{i}\}\},k)\mid i\geq 2,k\leq 2^{i}-3\bigr\}$
$\blacksquare$

$W_{D}^{3}:=\bigl\{(\{\{2_{i},4_{i}\},\{1_{i},5_{i}\}\},k)\mid i\geq 2,k\leq 2^% {i}-4\bigr\}$
$\blacksquare$

$W_{D}^{4}:=\bigl\{(\{\{2_{i},7_{i}\},\{3_{i},6_{i}\}\},k)\mid i\geq 2,k\leq 2^% {i}-4\bigr\}$
$\blacksquare$

$W_{D}^{5}:=\bigl\{(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k)\mid i\geq 2,k\leq 2^% {i}-4\bigr\}$
$\blacksquare$

$W_{D}^{6}:=\bigl\{(\{\{1_{i}\},\{2_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}\bigr\}$
$\blacksquare$

$W_{D}^{7}:=\bigl\{(\{\{2_{i}\},\{3_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}\bigr\}$
$\blacksquare$

$W_{D}^{8}:=\bigl\{(\{\{4_{i}\},\{5_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}-1\bigr\}$
$\blacksquare$

$W_{D}^{9}:=\bigl\{(\{\{6_{i}\},\{7_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}-1\bigr\}$

Then $W_{D}=\bigcup\limits_{0\leq j\leq 9}W_{D}^{j}$ is defined as the union of these sets. For $n\geq 1$ it is easy to see, that $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)\in W_{D}^{1}$ and thus $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)\in W_{D}$ holds. It is also easy to see that no $W_{D}^{j}$ contains a position $(\{A,B\},k)$ with $A=B=\emptyset$ . So $W_{D}$ does not contain any immediate winning position for $S$ . Player $D$ can also stop player $S$ from leaving $W_{D}$ . More precisely if $S$ makes a move from any position in $W_{D}$ , then $D$ can answer in such a way that the follow-up position is also in $W_{D}$ . We can prove this fact by going through all positions within $W_{D}$ and checking every possible move that $S$ can make. In this shortened proof we will showcase this for the set $W_{D}^{2}$ . The remaining cases are given as part of the appendix.

So let $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i}-3$ be some position from $W_{D}^{2}$ . In this position player $S$ can play an operator-move, where he picks some successor of $2_{i}$ . If he picks a node that is also a successor of $1_{i}$ or $3_{i}$ , then $D$ can answer by picking the same node. In this case the next position $(\{A,B\},k-1)$ satisfies $A\cap B\neq\emptyset$ . So it belongs to $W_{D}^{0}$ . Then $S$ cannot leave $W_{D}$ by picking a shared successor, meaning a node that is a successor of both sets of the position. So for $\mathcal{M}_{t,r}$ in particular we can ignore all moves where $S$ picks a node two or more layers below any of the current nodes. Every successor of $2_{i}$ besides $2_{i}$ itself is also a successor of $1_{i}$ or $3_{i}$ . If $S$ picks $2_{i}$ as its own successor then $D$ can answer by also using the self-loops of $1_{i}$ and $3_{i}$ . So this move leads to the new position $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k-1)$ , which is also a part of $W_{D}^{2}$ . Alternatively $S$ can also play an operator-move where he picks successors of $1_{i}$ and $3_{i}$ . Once again if $S$ picks a node that can also be picked by $D$ , then the next position is a member of $W_{D}^{0}$ . The only other options of $S$ are to pick $1_{i}$ or $6_{i}$ as a successor of $1_{i}$ and $3_{i}$ or $5_{i}$ as a successor of $3_{i}$ . If he uses the self-loop both times, $D$ answers with her own self-loop and the follow-up position belongs to $W_{D}^{2}$ . If $S$ choose $1_{i}$ and $5_{i}$ then $D$ answers $\{2_{i},4_{i}\}$ . This moves the play to $(\{\{2_{i},4_{i}\},\{1_{i},5_{i}\}\},k-1)$ , a position from $W_{D}^{3}$ . On the other hand if $S$ picked $6_{i}$ and $3_{i}$ , then $D$ answers with $\{2_{i},7_{i}\}$ , which leads to $(\{\{2_{i},7_{i}\},\{3_{i},6_{i}\}\},k-1)$ , a member of $W_{D}^{4}$ . Lastly if he choose $5_{i}$ and $6_{i}$ , $D$ picks $\{4_{i},7_{i}\}$ . The new position $(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k-1)$ belongs to $W_{D}^{5}$ . So $S$ cannot leave $W_{D}$ from $W_{D}^{2}$ by playing an operator-move.

At $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k)$ $S$ can also play a split-move. In this case he has to split $\{1_{i},3_{i}\}$ into $\{1_{i}\}$ and $\{3_{i}\}$ . He also splits the parameter $k$ into $k_{1}$ and $k_{2}$ . One of these two new parameters is at most half of the original parameter $k$ . So $D$ can pick $j$ in such a way, that $k_{j}\leq 2^{i-1}$ . Then she answers with $\{2_{i}\}$ . The new position of the play is either $(\{\{1_{i}\},\{2_{i}\}\},k_{j})\in W_{D}^{6}$ or $(\{\{2_{i}\},\{3_{i}\}\},k_{j})\in W_{D}^{7}$ . So we have shown that $S$ cannot leave $W_{D}$ by making a move in a position from $W_{D}^{2}$ .

The same holds for all other positions from $W_{D}$ . Since $S$ cannot leave $W_{D}$ and $W_{D}$ does not contain any immediate winning position, $S$ cannot win from any of these positions. Then all positions in $W_{D}$ are winning positions for $D$ . This includes $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)$ . So there cannot be a separating formula for $\{a_{n}\}$ and $\{b_{n}\}$ with $2^{n}-2$ or less modal operators. $\hfill\blacktriangleleft$

Theorem 11.

The logic ML $[\leftrightarrow]$ is exponentially more operator-succinct and exponentially more succinct than ML on the class of Kripke structures with a transitive and reflexive accessibility relation.

Proof.

Let $n\in\mathbb{N}$ be some natural number. Then $\psi_{n}$ is the ML $[\leftrightarrow]$ -formula given in Lemma 9. We know $|\psi_{n}|_{O}=g_{1}(n)\geq n$ and $|\psi_{n}|=g_{2}(n)\geq n$ for some polynomial functions $g_{1}$ and $g_{2}$ . We also know that $\psi_{n}$ separates the two transitive and reflexive Kripke structures $(\mathcal{M}_{t,r},a_{n})$ and $(\mathcal{M}_{t,r},b_{n})$ from one another. Let $\chi_{n}$ be some ML-formula equivalent to $\psi_{n}$ on the class of Kripke structures with a transitive and reflexive accessibility relation. Then $\chi_{n}$ has to be a separating formula for $(\mathcal{M}_{t,r},a_{n})$ and $(\mathcal{M}_{t,r},b_{n})$ as well. So, according to Lemma 10, $|\chi_{n}|_{O}\geq h(n)$ for some exponential function $h$ . This implies $|\chi_{n}|\geq h(n)$ as well. We define $f_{1}\colon\mathbb{N}\rightarrow\mathbb{N}$ as $f_{1}(n)=h\left(\lfloor(g_{1})^{-1}(n)\rfloor\right)$ . Then $|\chi_{n}|_{O}\geq h(n)\geq h\left(\lfloor(g_{1})^{-1}(|\psi_{n}|_{O})\rfloor% \right)=f_{1}\left(|\psi_{n}|_{O}\right)$ holds. So ML $[\leftrightarrow]$ is $f_{1}$ -times more operator-succinct than ML and thus exponentially more operator-succinct. We also define $f_{2}\colon\mathbb{N}\rightarrow\mathbb{N}$ as $f_{2}(n)=h\left(\lfloor(g_{2})^{-1}(n)\rfloor\right)$ . We know $|\chi_{n}|\geq f_{2}\left(|\psi_{n}|\right)$ holds. This implies that ML $[\leftrightarrow]$ is $f_{2}$ -times more succinct than ML, so it is exponentially more succinct as well. $\hfill\blacktriangleleft$

From this theorem it is easy to infer, that the succinctness gap also exists on all classes of structures, which are supersets of the class of Kripke structures with a transitive and reflexive accessibility relation. We say an accessibility relation $R$ is serial, if it satisfies the condition $\forall x\exists y:R(x,y)$ . It is called weakly dense, if it satisfies $\forall x\forall y:(R(x,y)\rightarrow\exists z:(R(x,z)\land R(z,y))$ . Both of these conditions are true for every reflexive relation.

Corollary 12.

The logic ML $[\leftrightarrow]$ is exponentially more succinct than ML on the following classes of pointed Kripke structures:

1.

The class of all pointed Kripke structures.
2.

The class of all pointed Kripke structures with a transitive accessibility relation.
3.

The class of all pointed Kripke structures with a reflexive accessibility relation.
4.

The class of all pointed Kripke structures with a serial accessibility relation.
5.

The class of all pointed Kripke structures with a weakly dense accessibility relation.

4.2 Symmetrical and reflexive graphs

The graph $\mathcal{M}_{s,r}$ is also constructed as an extension of $\mathcal{M}=(W,R,V)$ . We do not change the nodes or their labels. We only add edges to $\mathcal{M}$ . For every edge $(x,y)\in R$ we add its inverse $(y,x)$ to our new graph. For nodes $x$ and $y$ , that belong to the same level, we also add the edges $(x,y)$ and $(y,x)$ . This explicitly includes all possible self-loops. So formally $R_{s,r}=R\cup\{(y,x)\mid(x,y)\in R\}\cup\{(x,y)\mid\exists i\in\mathbb{N}% \colon\text{$x$ and $y$ belong to layer $i$}\}$ . It is easy to see that $\mathcal{M}_{s,r}$ is both symmetrical and reflexive.

Lemma 13.

There are two polynomial functions $g_{1},g_{2}\colon\mathbb{N}\rightarrow\mathbb{N}$ , so that for every $n\in\mathbb{N}$ there is an ML $[\leftrightarrow]$ -formula $\psi_{n}$ , which separates $(\mathcal{M}_{s,r},a_{n})$ from $(\mathcal{M}_{s,r},b_{n})$ , with $|\psi_{n}|_{O}=g_{1}(n)\geq n$ and $|\psi_{n}|=g_{2}(n)\geq n$ .

Proof.

Once again this is proven by adapting $\varphi_{n}$ from Claim 8. All edges in $\mathcal{M}$ go down exactly one layer. But all of the edges added to $R$ during the construction of $R_{s,r}$ either go up one layer or stay on the same layer. Since we used the labels $q_{0}$ , $q_{1}$ and $q_{2}$ in an alternating pattern, the current layer, the layer one below and the layer one above are all coloured differently. This means we can use these labels to make sure that only the original edges from $R$ are considered. We define $\psi_{n}$ via $\psi_{0}:=p_{0}$ and $\psi_{i}:=\Diamond(q_{1}\land\Box(\lnot q_{2}\lor((\Diamond(p_{1}\land q_{0})% \leftrightarrow(\Diamond(\psi_{i-1}\land q_{0})))))$ . For all nodes $w$ of layer $3n$ we know that $(\mathcal{M}_{s,r},w)\models\psi_{n}$ holds if, and only if, $(\mathcal{M},w)\models\varphi_{n}$ . So, by Claim 8, $\psi_{n}$ is a separating formula for $(\mathcal{M}_{s,r},a_{n})$ and $(\mathcal{M}_{s,r},b_{n})$ with $|\psi_{n}|_{O}=|\psi_{n-1}|_{O}+4$ and $|\psi_{n}|=|\psi_{n-1}|+15$ . So $g_{1}(n)=4\cdot n$ and $g_{2}(n)=15\cdot n+1$ fulfil all conditions of the lemma. $\hfill\blacktriangleleft$

Lemma 14.

There is an exponential function $h:\mathbb{N}\rightarrow\mathbb{N}$ , so that for every $n\in\mathbb{N}$ and for every ML-formula $\chi_{n}$ , which separates $\{(\mathcal{M}_{s,r},a_{n})\}$ from $\{(\mathcal{M}_{s,r},b_{n})\}$ , we have $|\chi_{n}|_{O}>h(n)$ .

Proof.

This proof is very similar to that of Lemma 10. We also use $h(n)=2^{n}-2$ , so $|\chi_{0}|_{O}>-1=h(0)$ holds. Then for $n\geq 1$ we show that $(\{\{a_{n}\},\{b_{n}\}\},h(n))$ is a winning position for player $D$ in the $\mathcal{M}_{s,r}$ -ON game. For this purpose we define the following sets of positions of the $\mathcal{M}_{s,r}$ -ON game.

$\blacksquare$

$W_{D}^{0}:=\bigl\{(\{A,B\},k)\mid A,B\subseteq W,A\cap B\neq\emptyset,k\in% \mathbb{N}\bigr\}$
$\blacksquare$

$W_{D}^{1}:=\bigl\{(\{\{a_{i}\},\{b_{i}\}\},k)\mid i\geq 1,k\leq 2^{i}-2\bigr\}$
$\blacksquare$

$W_{D}^{2}:=\bigl\{(\{\{2_{i}\},\{1_{i},3_{i}\}\},k)\mid i\geq 2,k\leq 2^{i}-3\bigr\}$
$\blacksquare$

$W_{D}^{3}:=\bigl\{(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k)\mid i\geq 2,k\leq 2^% {i}-4\}$
$\blacksquare$

$W_{D}^{4}:=\bigl\{(\{\{1_{i}\},\{2_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}\bigr\}$
$\blacksquare$

$W_{D}^{5}:=\bigl\{(\{\{1_{i}\},\{3_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}\bigr\}$
$\blacksquare$

$W_{D}^{6}:=\bigl\{(\{\{2_{i}\},\{3_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}\bigr\}$
$\blacksquare$

$W_{D}^{7}:=\bigl\{(\{\{4_{i}\},\{5_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}-1\bigr\}$
$\blacksquare$

$W_{D}^{8}:=\bigl\{(\{\{6_{i}\},\{7_{i}\}\},k)\mid i\geq 2,k\leq 2^{i-1}-1\bigr\}$

Then $W_{D}:=\bigcup\limits_{0\leq j\leq 8}W_{D}^{j}$ is defined as the union of these sets. For $n\geq 1$ it is easy to see that $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)\in W_{D}^{1}$ and thus $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)\in W_{D}$ holds. It is also easy to see, that no $W_{D}^{j}$ contains a position $(\{A,B\},k)$ with $A=B=\emptyset$ , so $W_{D}$ does not contain any immediate winning position for $S$ . Next we show that for every move of $S$ from a position of $W_{D}$ player $D$ can defend in such a way that the next position is in $W_{D}$ as well. In this shortened version of our proof we will only give a proper explanation for $W_{D}^{2}$ . The description of the other cases is once again moved to the appendix.

So we have to look at positions $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i}-3$ . Once again if $S$ picks a shared successor, $D$ can move the game to a position from $W_{D}^{0}$ . For $\mathcal{M}_{s,r}$ this happens every time $S$ picks a node of the same layer as any node in the other set. In particular if $S$ uses the self-loop on any nodes. Since every successor of $2_{i}$ is also a successor of $1_{i}$ or $3_{i}$ , player $S$ cannot leave $W_{D}$ by playing an operator-move on $\{2_{i}\}$ . Similarly when playing on $\{1_{i},3_{i}\}$ we only have to look at $S$ picking $b_{i}$ or $6_{i}$ as a successor of $1_{i}$ , as well as $b_{i}$ or $5_{i}$ as a successor of $3_{i}$ . This is because every other successor is also a successor of $2_{i}$ . If $S$ picked $b_{i}$ at all, then $D$ answers with $\{a_{i}\}$ . If he choose $5_{i}$ or $6_{i}$ in addition to $b_{i}$ , then these nodes will be removed when tidying up, because they are labelled differently from $a_{i}$ and $b_{i}$ . So in this case the game continues with $(\{\{a_{i}\},\{b_{i}\}\},k-1)$ , a position from $W_{D}^{1}$ . On the other hand, if $S$ picked both $5_{i}$ and $6_{i}$ as successors, $D$ answers with $\{4_{i},7_{i}\}$ . Then the follow-up position is $(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k-1)$ from $W_{D}^{3}$ . So $S$ cannot leave $W_{D}$ by playing an operator-move at $W_{D}^{2}$ . Lastly we look at what happens when $D$ plays a split-move. He has to split $\{1_{i},3_{i}\}$ into $\{1_{i}\}$ and $\{3_{i}\}$ and $k$ into $k_{1}$ and $k_{2}$ . Then $D$ can answer in such a way that $k_{j}\leq 2^{i-1}$ and the follow-up position is either $(\{\{1_{i}\},\{2_{i}\}\},k_{j})\in W_{D}^{4}$ or $(\{\{2_{i}\},\{3_{i}\}\},k_{j})\in W_{D}^{6}$ . With this we have shown that $S$ cannot leave $W_{D}$ in one move from $W_{D}^{2}$ .

The same goes for all other positions from $W_{D}$ . So $D$ can stop $S$ from leaving $W_{D}$ and there is no immediate winning position for $S$ in $W_{D}$ . Then all position in $W_{D}$ , including $(\{\{a_{n}\},\{b_{n}\}\},2^{n}-2)$ , have to be winning positions for player $D$ . This is why there cannot be a separating formula for $\{a_{n}\}$ and $\{b_{n}\}$ with $2^{n}-2$ or less modal operators. $\hfill\blacktriangleleft$

Theorem 15.

The logic ML $[\leftrightarrow]$ is exponentially more operator-succinct and exponentially more succinct than ML on the class of Kripke structures with a symmetrical and reflexive accessibility relation.

Proof.

The proof of this theorem can be done analogous to the proof of Theorem 11. Simply replace all mentions of transitivity with reflexivity and use Lemma 13 and Lemma 14 instead of Lemma 9 and Lemma 10 respectively. $\hfill\blacktriangleleft$

Since the succinctness gap exists when looking only at symmetrical and reflexive graphs, it has to exist for any class of graphs that contains all symmetrical and reflexive graphs.

Corollary 16.

The logic ML $[\leftrightarrow]$ is exponentially more succinct than ML on the class of Kripke structures with a symmetrical accessibility relation.

4.3 Transitive and symmetrical graphs

So far in this paper we have shown that adding bi-implications allows us to write more succinct formulas. Even when only looking at special classes of Kripke structures, like those with a transitive accessibility relation and those with a symmetrical one. In this section we are going to show that the same does not hold if we combine these two conditions. More precisely we show that there is no exponential succinctness gap between ML and ML $[\leftrightarrow]$ on the class of Kripke structures with a transitive and symmetrical accessibility relation.

We start with a few remarks about our notation in this section. Let $\mathcal{S}_{S5}$ be the class of all Kripke structures with a transitive, symmetrical and reflexive accessibility relation. We write $\varphi\equiv_{T,S}\psi$ if $\varphi$ and $\psi$ are equivalent on all pointed Kripke structures with a transitive and symmetrical accessibility relation. Similarly we use $\equiv_{\mathcal{S}_{S5}}$ when talking about structures from $\mathcal{S}_{S5}$ and $\equiv_{E}$ for graphs with an empty accessibility relation.

All connected, transitive and symmetrical graphs, that are not reflexive as well, contain a single node and no edges. So $\varphi\equiv_{T,S}\psi$ holds if, and only if, both $\varphi\equiv_{\mathcal{S}_{S5}}\psi$ and $\varphi\equiv_{E}\psi$ hold. This fact offers us a way to find formulas that are equivalent on transitive and symmetrical structures, which we will use to prove the following Theorem.

Theorem 17.

For every ML $[\leftrightarrow]$ -formula $\varphi$ there is an ML-formula $\psi$ with $\varphi\equiv_{T,S}\psi$ and the size of $\psi$ is polynomial in the size of $\varphi$ .

Proof.

In [2] it is shown, that ML $[\leftrightarrow]$ has polynomial translations with regards to $\mathcal{S}_{S5}$ in ML. So for every ML $[\leftrightarrow]$ -formula $\varphi$ there is an ML-formula $\psi_{1}$ with $\varphi\equiv_{\mathcal{S}_{S5}}\psi_{1}$ and the size of $\psi_{1}$ is polynomial in the size of $\varphi$ . We now look at the graph with only one node and no edges. We know $\Diamond\chi\equiv_{E}\bot$ as well as $\Box\chi\equiv_{E}\top$ for all formulas $\chi$ . We can use this to replace all operators in $\varphi$ , obtaining a operator free formula $\psi^{\prime}$ with $\psi^{\prime}\equiv_{E}\varphi$ . Since this formula does not contain any operators, we can treat it as a formula of propositional logic. So as described by Pratt in [10], we can use Spira’s construction from [11] in order to construct an ML-formula $\psi_{2}$ with $\psi_{2}\equiv\psi^{\prime}\equiv_{E}\varphi$ . The size of $\psi_{2}$ is polynomial in the size of $\psi^{\prime}$ , which in turn is bounded from above by the size of $\varphi$ . Now we just need to combine these formulas to obtain $\psi$ . In order to do so we use the formula $\Diamond\top$ , which is true on all graphs from $\mathcal{S}_{S5}$ and false for all edgeless graphs, as well as its negation $\Box\bot$ . We construct the wanted ML-formula as $\psi:=(\psi_{1}\land\Diamond\top)\lor(\psi_{2}\land\Box\bot)$ . This formula fulfils the following:

\psi\equiv_{\mathcal{S}_{S5}}(\psi_{1}\land\Diamond\top)\lor(\psi_{2}\land\Box% \bot)\equiv_{\mathcal{S}_{S5}}(\psi_{1}\land\top)\lor(\psi_{2}\land\bot)\equiv% _{\mathcal{S}_{S5}}\psi_{1}\equiv_{\mathcal{S}_{S5}}\varphi

\psi\equiv_{E}(\psi_{1}\land\Diamond\top)\lor(\psi_{2}\land\Box\bot)\equiv_{E}% (\psi_{1}\land\bot)\lor(\psi_{2}\land\top)\equiv_{E}\psi_{2}\equiv_{E}\varphi

Which also implies $\psi\equiv_{T,S}\varphi$ . The size of this formula is $|\psi_{1}|+|\psi_{2}|+7$ , so the sum of two polynomials over $|\varphi|$ and a constant, which is also polynomial in the size of $\varphi$ . $\hfill\blacktriangleleft$

5 Conclusion

The main result of this paper is the development of a new model comparison game, the $\mathcal{M}$ -Operator-Number game. This game can be used to prove lower bounds for the number of modal operators necessary to express certain properties in modal logic. An interesting follow-up question to this might be: For which logics and which parameters can a similar game be designed? If there is a version of the Hella-Vilander game for some logic, it should be possible to adjust that game to only count all occurrences of one specific type of operator. This should work for every type of operator of that logic. The more interesting part of that question is whether or not some process similar to our idea of ’tidying up’ is possible. A positive answer is given for FO^l in [14]. However additional research is necessary to achieve a better understanding of this topic.

We also give a more complete overview of the succinctness of modal logic with bi-implication on different classes of Kripke structures. For every possible combination of the properties reflexive, transitive and symmetrical, we have either proven or disproven the existence of an exponential succinctness gap between ML and ML $[\leftrightarrow]$ on the corresponding class of structures.

A possible future task could be to look into even more classes of Kripke structures, for example those with a function or a partial function as accessibility relation. Although these examples might require a quite different proof from the ones presented in this paper. Instead we could also attempt to adjust our proofs for a different logic. Our current goal is to do this for the logic CTL. This logic can be seen as an extension of ML, where more complex operators are added. Our hope is that we can show that bi-implications can be used to write exponentially shorter formulas in CTL as well.

References

[1] Micah Adler and Neil Immerman. An $n!$ lower bound on formula size. ACM Transactions on Computational Logic, 4(3):296–314, 2003. doi:10.1145/772062.772064.
[2] Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Boolean basis, formula size, and number of modal operators. Logical Methods in Computer Science, Volume 21, Issue 3, July 2025. doi:10.46298/lmcs-21(3:10)2025.
[3] Marco Carmosino, Ronald Fagin, Neil Immerman, Phokion Kolaitis, Jonathan Lenchner, and Rik Sengupta. Multi-structural games and beyond. Logical Methods in Computer Scienc, 20:27:1–27:40, 2024. doi:10.48550/arXiv.2301.13329.
[4] Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129–141, 1960. URL: https://eudml.org/doc/213582.
[5] Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, and Nikhil Vyas. Multi-structural games and number of quantifiers. Logical Methods in Computer Science, 21(1), 2025. doi:10.46298/lmcs-21(1:10)2025.
[6] Roland Fraïssé. On some classifications of relationship systems. Publications scientifiques de l’Université d’Alger, Série A, Sciences mathématiques, 1954.
[7] Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. Succinctness of epistemic languages. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-11), pages 881–886, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-153.
[8] Martin Grohe and Nicole Schweikardt. The succinctness of first-order logic on linear orders. Logical Methods in Computer Science, 1(1), 2005. doi:10.2168/LMCS-1(1:6)2005.
[9] Lauri T. Hella and Miikka S. Vilander. Formula size games for modal logic and $\mu$ -calculus. Journal of Logic and Computation, 29(8):1311–1344, 2019. doi:10.1093/logcom/exz025.
[10] Vaughan R. Pratt. The effect of basis on size of boolean expressions. In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, pages 119–121, October 1975. doi:10.1109/SFCS.1975.29.
[11] Philip Spira. On time-hardware complexity tradeoffs for boolean functions. In Proceedings of the 4th Hawaii Symposium on System Sciences, 1971, pages 525–527, 1971.
[12] Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. On the relative succinctness of two extensions by definitions of multimodal logic. Lecture Notes in Computer Science, 7318 LNCS:323–333, 2012. doi:10.1007/978-3-642-30870-3_33.
[13] Hans van Ditmarsch, Jie Fan, Wiebe van der Hoek, and Petar Iliev. Some exponential lower bounds on formula-size in modal logic. In Advances in Modal Logic, volume 10, pages 139–157, August 2014. URL: https://www.scopus.com/inward/record.uri?eid=2-s2.0-84924671231&partnerID=40&md5=3f43caf649380733487e57e7338bd34d.
[14] Harry Vinall-Smeeth. From quantifier depth to quantifier number: Separating structures with $k$ variables. In Proceedings - Symposium on Logic in Computer Science, 2024. doi:10.1145/3661814.3662125.

Appendix A Appendix

A.1 Proof of Lemma 2

$\vartriangleright$ Claim of Lemma 2. Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph and $A,B,A^{\prime},B^{\prime}\subseteq W$ be sets of nodes with $t(\{A,B\})=\{A^{\prime},B^{\prime}\}$ . If there is a separating formula $\varphi^{\prime}$ for $(\mathcal{M},A^{\prime})$ and $(\mathcal{M},B^{\prime})$ , then there is also a separating formula $\varphi$ for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ with $|\varphi|_{O}=|\varphi^{\prime}|_{O}$ .

Proof.

Without loss of generality we assume $A^{\prime}\subseteq A$ and $B^{\prime}\subseteq B$ . In order to prove this lemma, we look at the sets $A^{\prime\prime}=A\setminus A^{\prime}$ and $B^{\prime\prime}=B\setminus B^{\prime}$ . We know that no node in $A^{\prime\prime}$ has the same colour as any node in $B$ and no node in $B^{\prime\prime}$ has the same color as any node in $A$ . It is easy to see that two pointed Kripke structures based on differently coloured nodes can be separated by a literal. In this case let $\psi_{a,b}$ be a literal with $(\mathcal{M},a)\models\psi_{a,b}$ and $(\mathcal{M},b)\not\models\psi_{a,b}$ . Then for every $a\in A^{\prime\prime}$ we define $\Psi_{a}:=\{\psi_{a,b}\mid b\in B\}$ . All nodes in $W$ agree on all labels that are not used in $\mathcal{M}$ . Then every formula in $\Psi_{a}$ must be either an atomic formula from $V(W)$ or the negation of such an atomic formula. So even though $B$ might be infinite, $\Psi_{a}$ will always be finite, since $V(W)$ is finite. So we can construct the formula $\psi_{a}:=\bigwedge\limits_{\psi_{a,b}\in\Psi_{a}}\psi_{a,b}$ , which separates $(\mathcal{M},a)$ from $(\mathcal{M},B)$ . Next we look at the set $\Psi:=\{\psi_{a}\mid a\in A^{\prime\prime}\}$ and the formula $\psi:=\bigvee\limits_{\psi_{a}\in\Psi}\psi_{a}$ . This formula $\psi$ holds in $(\mathcal{M},A^{\prime\prime})$ , while its negation holds in $(\mathcal{M},B)$ .

In a similar fashion we define $X_{b}:=\{\psi_{a,b}\mid a\in A\}$ and $\chi_{b}:=\bigvee\limits_{\psi_{a,b}\in X_{b}}\psi_{a,b}$ for every $b\in B^{\prime\prime}$ . Next we construct $X:=\{\chi_{b}\mid b\in B^{\prime\prime}\}$ and $\chi:=\bigwedge\limits_{\chi_{b}\in X}\chi_{b}$ . This formula holds in $(\mathcal{M},A)$ and its negation holds in $(\mathcal{M},B^{\prime\prime})$ . With this we can finally define the wanted formula $\varphi$ . Without loss of generality we assume $(\mathcal{M},A^{\prime})\models\varphi^{\prime}$ . Then $\varphi=(\varphi^{\prime}\land\chi)\lor\psi$ is a separating formula for $(\mathcal{M},A)$ and $(\mathcal{M},B)$ . Since neither $\psi$ nor $\chi$ contain any operators, $|\varphi|_{O}=|\varphi^{\prime}|_{O}$ holds as well. $\hfill\vartriangleleft$

A.2 Proof of Lemma 3

$\vartriangleright$ Claim of Lemma 3. Let $\mathcal{M}=(W,R,V)$ be a finitely labelled graph, $A,B\subseteq W$ be sets of nodes that form a tidy pair and let $\varphi$ be an ML-formula without any modal operators. Then $(\mathcal{M},A)\models\varphi$ if, and only if, $(\mathcal{M},B)\models\varphi$ .

Proof.

If $A=B=\emptyset$ , then the Lemma is trivially true. Otherwise let $(\mathcal{M},A)\models\varphi$ . For every $b\in B$ there is a $a\in A$ with $V(a)=V(b)$ . Then $a$ and $b$ agree on all atomic formulas and thus on all operator-free ML-formulas, so especially on $\varphi$ . This means $(\mathcal{M},b)\models\varphi$ for every $b\in B$ and thus $(\mathcal{M},B)\models\varphi$ . The converse implication follows from $\{A,B\}=\{B,A\}$ . $\hfill\vartriangleleft$

A.3 Proof of Lemma 7

During the proof of Lemma 7 we sketch a method that removes all $\leftrightarrow$ from an ML $[\leftrightarrow]$ -formula, while guaranteeing an exponential increase at most in the number of modal operators. Here we give a proper formal definition of this construction. We also prove its correctness.

Proof.

We recursively define a function $f\colon$ ML $[\leftrightarrow]\rightarrow$ ML $[\leftrightarrow]$ . The base case consist of all formulas $\varphi$ without any operators and in this case $f(\varphi):=\varphi$ . For any other formula $\varphi$ there must be a sub-formula $\chi$ so that $\Diamond\chi$ appears in $\varphi$ outside of the scope of any other operator. Then $\varphi$ can be written as $\psi(\Diamond\chi)$ for some formula $\psi$ . We define $f(\varphi)$ as $f(\varphi):=(f(\psi(\top))\land\Diamond f(\chi))\lor(f(\psi(\bot))\land\lnot% \Diamond f(\chi))$ .

Next we want to show that $f(\varphi)$ fulfils the following three conditions for every ML $[\leftrightarrow]$ formula $\varphi$ : Firstly $f(\varphi)\equiv\varphi$ , secondly no operator in $f(\varphi)$ appears in the scope of any bi-implication and thirdly $|f(\varphi)|_{O}\leq 2^{|\varphi|_{O}}\cdot|\varphi|_{O}$ . We do this via induction on the number of operators in $\varphi$ . As our base case we look at all ML $[\leftrightarrow]$ formulas $\varphi$ with no modal operators. Then we know $f(\varphi)=\varphi$ , so the first condition is obviously fulfilled. Because $f(\varphi)$ does not contain any operators, the second condition is also trivially true and because of $|f(\varphi)|_{O}=|\varphi|_{O}=0$ , the third condition is also fulfilled.

For the induction step we look at all formulas $\varphi$ with $|\varphi|_{O}=i$ for some $i\geq 1$ . In this case let $\psi$ and $\chi$ be the sub-formulas with $\varphi=\psi(\Diamond\chi)$ , that were used when constructing $f(\varphi)$ . Because of $|\psi|_{O}<|\varphi|_{O}$ and $|\chi|_{O}<|\varphi|_{O}$ we may assume as our induction hypothesis that both $f(\psi)$ and $f(\chi)$ fulfil all three conditions. Then we know $\varphi\equiv(\psi(\top)\land\Diamond\chi)\lor(\psi(\bot)\land\lnot\Diamond\chi)$ . Because of $f(\psi)\equiv\psi$ and $f(\chi)\equiv\chi$ , this is equivalent to $(f(\psi(\top))\land\Diamond f(\chi))\lor(f(\psi(\bot))\land\lnot\Diamond f(% \chi))=f(\varphi)$ . No operator in $f(\psi)$ or in $f(\chi)$ appears in the scope of any bi-implication. So the same must hold for $f(\varphi)$ , since no new bi-implication is added during its construction. For the number of operators we know $|\varphi|_{O}=|\psi|_{O}+|\chi|_{O}+1$ and $|f(\varphi)|_{O}=2\cdot|f(\psi)|_{O}+2\cdot|f(\chi)|_{O}+2$ . So by our induction hypothesis we know that $|f(\varphi)|_{O}\leq 2^{|\psi|_{O}+1}\cdot|\psi|_{O}+2^{|\chi|_{O}+1}\cdot|% \chi|_{O}+2$ . The value of the right hand side of this inequality becomes largest if all but one operators of $\varphi$ belong to the same sub-formula. So it is bounded from above by $2^{|\varphi|_{O}}\cdot(|\varphi|_{O}-1)+2$ . For $|\varphi|_{O}\geq 1$ this is in turn bounded from above by $2^{|\varphi|_{O}}\cdot|\varphi|_{O}$ . So the third condition is fulfilled as well.

In total we have shown that for every ML $[\leftrightarrow]$ -formula $\varphi$ there exists an equivalent ML $[\leftrightarrow]$ -formula $f(\varphi)$ where no operator appears in the scope of a bi-implication and the number of operators in $\varphi^{\prime}$ is at most exponential in the number of operators in $\varphi$ . Lastly we can replace every sub-formula $\psi\leftrightarrow\chi$ in $f(\varphi)$ with $(\psi\land\chi)\lor(\lnot\psi\land\lnot\chi)$ , in order to transform $f(\varphi)$ into an ML-formula, without increasing the number of operators any further. This construction proves, that the operator-succinctness gap between ML and ML $[\leftrightarrow]$ is at most exponential. $\hfill\blacktriangleleft$

A.4 Proof of Lemma 10

During the proof of Lemma 10 we claimed that player $D$ can ensure that a play of the game never leaves the set $W_{D}$ . Here we want to give a complete proof of this fact.

Proof.

We begin with some general facts. Since $\mathcal{M}_{t,r}$ is reflexive, player $S$ can always play an operator-move, where he picks every node as its own successor. However $D$ can answer by doing the same. So the follow up position consists of the same pair of sets as the current position only with the parameter reduced by one. So the new position belongs to the same set as the old position. Also $S$ cannot play a split-move, as long as both sets of the current position contain only one element each.

We start with $W_{D}^{0}$ . So let $(\{A,B\},k)\in W_{D}^{0}$ be some position and let $w\in A\cap B$ be some node shared between $A$ and $B$ . For $k\geq 2$ , $S$ can play a split-move in this position. He picks $X\in\{A,B\}$ and then splits this set into $X_{1}$ and $X_{2}$ . Then the shared node $w$ has to be in one of these two sets, w.l.o.g. we can assume $w\in X_{1}$ . Then $D$ can ensure $w\in Y^{\prime}$ for her answer and the game continues from the position $(t(\{X_{1},Y^{\prime}\}),k_{1})$ . The node $w$ is also a shared node for $X_{1}$ and $Y^{\prime}$ . For this reason $w$ cannot be removed by tidying up, because there will always be a node of the same colour in the respective other set, namely $w$ itself. So in the position after the move, the two sets still have $w$ as a shared node. Then this new position lies in $W_{D}^{0}$ as well and thus in $W_{D}$ . On the other hand $S$ might play an operator-move instead. In this case he picks $X\in\{A,B\}$ and then for every $x\in X$ he picks a successor $f(x)$ . Because of $w\in Y$ , we know $f(w)\in\Box Y$ . So $D$ can ensure $f(w)\in Y^{\prime}$ . Then $f(w)$ is a shared node for $X^{\prime}$ and $Y^{\prime}$ and thus it is not removed by tidying up. This means that the follow-up position $(t(\{X^{\prime},Y^{\prime}\}),k-1)$ is also a member of $W_{D}^{0}$ and of $W_{D}$ . So $D$ can ensure that the $\mathcal{M}_{s,r}$ -ON game cannot move from a position inside of $W_{D}^{0}$ to a position outside of $W_{D}$ .

During an operator-move, if $S$ tries to pick some node $x^{\prime}$ as $f(x)$ with $x^{\prime}\in\Box Y$ , the $D$ can ensure $x^{\prime}\in Y^{\prime}$ . So $x^{\prime}$ is a shared node for the new position and thus this position is a part of $W_{D}^{0}$ . Then $S$ cannot leave $W_{D}$ by playing like this. So from now on we may ignore all of his moves where he picks some shared successor. This is especially relevant, because in $\mathcal{M}_{t,r}$ all nodes that are two or more layers below the current node are successors of the current node. So every move where $D$ picks some node that is two or more layers below any node from $Y$ leads to a position from $W_{D}^{0}$ . For the rest of this proof we may ignore every move of $S$ with this property.

Next we look at $W_{D}^{1}$ . Let $(\{\{a_{i}\},\{b_{i}\}\},k)$ be a position with $i\geq 1$ and $k\leq 2^{i}-2$ . For $i=1$ we know $k=0$ . So $S$ cannot play any moves, meaning he cannot leave $W_{D}$ . So from now on we can assume $i>1$ . Then $S$ has to play an operator-move in such a position. However every successor of $b_{i}$ is either $b_{i}$ itself or a successor of $b_{i}$ as well. Also the only successor of $a_{i}$ that is not a successor of $b_{i}$ as well is $2_{i}$ . So $S$ has to pick $2_{i}$ as a successor of $a_{i}$ . To this $D$ answers with $\{1_{i},3_{i}\}$ and the follow-up position $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k-1)$ is a part of $W_{D}^{2}$ .

We already gave a detailed explanation for $W_{D}^{2}$ during the main proof, so we will skip it here.

Now we look at $W_{D}^{3}$ , which contains positions $(\{\{2_{i},4_{i}\},\{1_{i},5_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i}-4$ . Every successor of $4_{i}$ is also a successor of $1_{i}$ as well, including $4_{i}$ itself. So we can ignore all operator-moves, where $S$ tries to pick successors for $2_{i}$ and $4_{i}$ . Similarly every proper successor of $5_{i}$ is also a successor of $2_{i}$ . This means we only need to look at $S$ picking $5_{i}$ as a successor of itself and $6_{i}$ as successor of $1_{i}$ . Then $D$ answers with $\{4_{i},7_{i}\}$ and the new position $(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k-1)$ belongs to $W_{D}^{5}$ . $S$ can also play a split-move, where he either splits $\{2_{i},4_{i}\}$ into $\{2_{i}\}$ and $\{4_{i}\}$ or $\{1_{i},5_{i}\}$ into $\{1_{i}\}$ and $\{5_{i}\}$ . Either way he also has to split $k$ into $k_{1}$ and $k_{2}$ . Because of $k\leq 2^{i}-4$ , $D$ can always pick a $j\in\{1,2\}$ so that $k_{j}\leq 2^{i-1}-1$ . The set $D$ picks depends on the choice of $X_{j}$ . She answers with $\{2_{i}\}$ to $\{1_{i}\}$ and the other way around. Then the follow-up position $(\{\{1_{i}\},\{2_{i}\}\},k_{j})$ is a member of $W_{D}^{6}$ . On the other hand $D$ picks $\{5_{i}\}$ as an answer to $\{4_{i}\}$ and vice versa. In this case the play moves to $(\{\{4_{i}\},\{5_{i}\}\},k_{j})$ , which belongs to $W_{D}^{8}$ . Either way $S$ cannot leave $W_{D}$ from $W_{D}^{3}$ .

For the next set, $W_{D}^{4}$ , we look at positions $(\{\{2_{i},7_{i}\},\{3_{i},6_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i}-4$ . The arguments for these positions are very similar to those used for $W_{D}^{3}$ . Every successor of $7_{i}$ is also a successor of $3_{i}$ and every proper successor of $6_{i}$ is a successor of $2_{i}$ . So the only operator-move we need to look at is $S$ picking $5_{i}$ as a successor of $3_{i}$ and $6_{i}$ as its own successor. To this $D$ answers with $\{4_{i},7_{i}\}$ The follow-up position is $(\{\{4,7\},\{5,6\}\},k-1)$ and belongs to $W_{D}^{5}$ . $S$ can also either split $\{2_{i},7_{i}\}$ into $\{2_{i}\}$ and $\{7_{i}\}$ or he can split $\{3_{i},6_{i}\}$ into $\{3_{i}\}$ and $\{6_{i}\}$ . Either way $D$ can always guarantee $k_{j}\leq 2^{i-1}-1$ for some $j\in\{1,2\}$ . Then she can answer in such a way that the next position is either $(\{\{2_{i}\},\{3_{i}\}\},k_{j})$ from $W_{D}^{7}$ or $(\{\{6_{i}\},\{7_{i}\}\},k_{j})$ from $W_{D}^{9}$ . So $S$ cannot leave $W_{D}$ from $W_{D}^{4}$ either.

$W_{D}^{5}$ contains all positions $(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i}-4$ . Every proper successor of $4_{i}$ or $7_{i}$ is also a successor of $5_{i}$ or $6_{i}$ and vice versa. So we already know that every operator-move leads to a position from $W_{D}$ . However $S$ can also play a split move. He either splits $\{4_{i},7_{i}\}$ into $\{4_{i}\}$ and $\{7_{i}\}$ or he splits $\{5_{i},6_{i}\}$ into $\{5_{i}\}$ and $\{6_{i}\}$ . He also splits the parameter $k$ into $k_{1}$ and $k_{2}$ . Then $D$ can always pick $j\in\{1,2\}$ in such a way that $k_{j}\leq 2^{i-1}-1$ . She can also choose $Y^{\prime}$ in such a way that the follow-up position is either $(\{\{4_{i}\},\{5_{i}\}\},k_{j})$ , which belongs to $W_{D}^{8}$ , or $(\{\{6_{i}\},\{7_{i}\}\},k_{j})$ , a member of $W_{D}^{9}$ .

The next set we look at is $W_{D}^{6}$ , which contains positions $(\{\{1_{i}\},\{2_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}$ . Here $S$ has to play an operator-move. Since we can ignore all shared successors, the only moves we need to look at are picking $6_{i}$ as a successor of $1_{i}$ and picking $7_{i}$ as a successor of $2_{i}$ . In any case $D$ answers with the respective other node. Then the new position is $(\{\{6_{i}\},\{7_{i}\}\},k-1)\in W_{D}^{9}$ .

In positions $(\{\{2_{i}\},\{3_{i}\}\},k)$ from $W_{D}^{7}$ $S$ has to play an operator-move as well. The only moves we need to check are $S$ picking $4_{i}$ as a successor of $2_{i}$ or $5_{i}$ as a successor of $3_{i}$ . In either case $D$ can guarantee $(\{\{4_{i}\},\{5_{i}\}\},k-1)$ , a position from $W_{D}^{8}$ , as the follow-up position.

The set $W_{D}^{8}$ contains positions $(\{\{4_{i}\},\{5_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}-1$ . In such a position $S$ has to play an operator-move. Aside from picking shared successors or using only self-loops, $S$ can only pick $a_{i-1}$ as a successor of $4-i$ or $b_{i-1}$ as a successor of $5_{i}$ . Then $D$ answers with whatever node $S$ did not pick and the next position is $(\{\{a_{i-1}\},\{b_{i-1}\}\},k-1)$ , a member of $W_{D}^{2}$ .

Lastly we look at the set $W_{D}^{9}$ , so positions $(\{\{6_{i}\},\{7_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}-1$ . We only need to check what happens when $S$ picks either $a_{i-1}$ as a successor of $6_{i}$ or $b_{i-1}$ as a successor of $7_{i}$ . Independent of his choice, $D$ can guarantee $(\{\{a_{i-1}\},\{b_{i-1}\}\},k-1)\in D_{W}^{1}$ as the new position. $\hfill\blacktriangleleft$

A.5 Proof of Lemma 14

During the proof of Lemma 14 we stated that player $D$ can ensure that it is impossible to leave the set $W_{D}$ by playing a move of the $\mathcal{M}_{s,r}$ -ON game. Here we want to give a complete proof of this fact.

Proof.

During the proof of Lemma 10 we showed that in $\mathcal{M}_{t,r}$ player $S$ cannot leave $W_{D}^{0}$ . The argumentation we used was completely independent from the actual edges of the graph. So we can use exactly the same argumentation here to show that $S$ cannot leave $W_{D}^{0}$ in $\mathcal{M}_{s,r}$ either. This also means that $S$ cannot leave $W_{D}$ by picking some shared successor. For $\mathcal{M}_{s,r}$ in particular this includes all moves, where he tries to pick a node of the current layer.

The next set we want to look at is $W_{D}^{1}$ . So let $(\{\{a_{i}\},\{b_{i}\}\},k)$ be a position with $i\geq 1$ and $k\leq 2^{i}-2$ . For $i=1$ we know $k=0$ . As already mentioned $S$ cannot make another move for $k=0$ , meaning he cannot leave $W_{D}$ . For $i\geq 2$ he cannot play a split-move, since both sets have only one element each. So he has to play an operator-move instead. Recall that the nodes $a_{i}$ and $b_{i}$ belong segment $i+1$ as well as to segment $i$ and since $\mathcal{M}_{s,r}$ is a symmetrical graph, these nodes also have successors in the layer above, layer $3i+1$ . Then $S$ can pick $4_{i+1}$ , $6_{i+1}$ or $2_{i}$ as a successor of $a_{i}$ . Alternatively he may pick $5_{i+1}$ or $7_{i+1}$ as a successor of $b_{i}$ . Every other successor of $a_{i}$ or $b_{i}$ is a shared successor. If he choose either $4_{i+1}$ or $5_{i+1}$ , then $D$ answers with a set that contains only the respective other node. This leads to the follow-up position $(\{\{4_{i+1}\},\{5_{i+1}\}\},k-1)$ . Because of $k-1\leq 2^{i}-3$ this position belongs to $W_{D}^{7}$ . Alternatively if $S$ picked $6_{i+1}$ or $7_{i+1}$ , then $D$ also answers with the respective other node. Then the follow-up position is $(\{\{6_{i+1}\},\{7_{i+1}\}\},k-1)$ , which belongs to $W_{D}^{8}$ . Lastly if $S$ decided to move from $a_{i}$ to $2_{i}$ , then $D$ answers with the set $\{1_{i},3_{i}\}$ which progresses the play to the position $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k-1)$ . This position belongs to $W_{D}^{2}$ . So independent of the choices made by $S$ , the play always continues from some position within $W_{D}$ .

We already checked $W_{D}^{2}$ during the main proof, so we skip it here.

We continue by analysing $W_{D}^{3}$ . Let $(\{\{4_{i},7_{i}\},\{5_{i},6_{i}\}\},k)$ be some position with $i\geq 2$ and $k\leq 2^{i}-4$ . If $S$ plays an operator-move from this position, he has to pick $2_{i}$ as a successor of both $4_{i}$ and $7_{i}$ , since every other successor is a shared successor. To this, $D$ answers with the set $\{1_{i},3_{i}\}$ . Then the follow-up position $(\{\{2_{i}\},\{1_{i},3_{i}\}\},k-1)$ belongs to $W_{D}^{2}$ . However for $k\geq 2$ , $S$ can also play a split-move. In this case he has to split either $\{4_{i},7_{i}\}$ into $\{4_{i}\}$ and $\{7_{i}\}$ or $\{5_{i},6_{i}\}$ into $\{5_{i}\}$ and $\{6_{i}\}$ . He also splits $k$ into $k_{1}$ and $k_{2}$ . Let $k_{j}$ be the smaller of these two. Then we know $k_{j}\leq 2^{i-1}-2$ . Then $D$ answers by picking the side with $k_{j}$ . The set she picks depends on what choice was made by $S$ for $X_{j}$ . She answers with $\{5_{i}\}$ to $\{4_{i}\}$ and vice versa. Similarly she picks $\{6_{i}\}$ as an answer to $\{7_{i}\}$ and the other way around. So the follow-up position is either $(\{\{4_{i}\},\{5_{i}\}\},k_{j})$ , which is a member of $W_{D}^{7}$ , or $(\{\{6_{i}\},\{7_{i}\}\},k_{j})$ , which is a member of $W_{D}^{8}$ . So $S$ cannot leave $W_{D}$ from $W_{D}^{3}$ either.

The next set is $W_{D}^{4}$ . So we look at a position $(\{\{1_{i}\},\{2_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}$ . In this position, $S$ cannot play a split-move, since both sets contain only one node each. This will be the case for all sets from this point on, so we will stop mentioning it going forward. Now player $S$ has to play an operator-move, where he picks $b_{i}$ or $6_{i}$ as a successor of $1_{i}$ or $7_{i}$ as a successor of $2_{i}$ . If he picked $b_{i}$ , $D$ answers with $\{a_{i}\}$ . This moves the game to $(\{\{a_{i}\},\{b_{i}\}\},k-1)$ . Because of $i\geq 2$ , which implies $2^{i-1}\leq 2^{i}-2$ , this position belongs to $W_{D}^{1}$ . On the other hand, if $S$ choose $6_{i}$ or $7_{i}$ , then $D$ answers with the set only containing the respective other node. Then the follow-up position is $(\{\{6_{i}\},\{7_{i}\}\},k-1)$ , which belongs to $W_{D}^{8}$ . Then $D$ can force any play from $W_{D}^{4}$ to stay in $W_{D}$ .

We continue our proof with $W_{D}^{5}$ . The positions within this set are the shape of $(\{1_{i}\},\{3_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}$ . When playing an operator-move, $S$ may pick $4_{i}$ or $6_{i}$ as a successor of $1_{i}$ or he may pick $5_{i}$ or $7_{i}$ as a successor of $3_{i}$ . Then $D$ answers with $\{5_{i}\}$ to $4_{i}$ , with $\{7_{i}\}$ to $6_{i}$ , with $\{4_{i}\}$ to $5_{i}$ and lastly with $\{6_{i}\}$ to $7_{i}$ . Then the play continues with $(\{\{4_{i}\},\{5_{i}\},k-1)$ , a position from $W_{D}^{7}$ , or with $(\{\{6_{i}\},\{7_{i}\}\},k-1)$ , a position from $W_{D}^{8}$ . This finishes the case of $W_{D}^{5}$ .

Now we look at the set $W_{D}^{6}$ , which contains all positions $(\{\{2_{i}\},\{3_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}$ . Here $S$ may pick $4_{i}$ as a successor of $2_{i}$ or alternatively $b_{i}$ or $5_{i}$ as a successor of $3_{i}$ . If he picked $b_{i}$ then $D$ answers with $\{a_{i}\}$ . Then the follow-up position $(\{\{a_{i}\},\{b_{i}\}\},k-1)$ is a member of $W_{D}^{1}$ . If $S$ choose $4_{i}$ or $5_{i}$ instead, then $D$ answers by picking a singleton of the respective other node. In this case the game moves on to the position $(\{\{4_{i}\},\{5_{i}\}\},k-1)$ , which belongs to $W_{D}^{7}$ .

The set $W_{D}^{7}$ consists of all positions $(\{\{4_{i}\},\{5_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}-1$ . Then $S$ can play an operator-move by picking $1_{i}$ , $2_{i}$ or $a_{i-1}$ as a successor of $4_{i}$ . Alternatively he may also pick $3_{i}$ or $b_{i-1}$ . If $S$ choose $2_{i}$ or $3_{i}$ , then $D$ answers with $\{3_{i}\}$ or $\{2_{i}\}$ respectively. This creates the follow-up position $(\{\{2_{i}\},\{3_{i}\}\},k-1)$ , which is a part of $W_{D}^{6}$ . If $S$ picked $1_{i}$ , then $D$ answers with $\{3_{i}\}$ , creating $(\{\{1_{i}\},\{3_{i}\}\},k-1)$ instead. This position belongs to $W_{D}^{5}$ . On the other hand if $S$ picked $a_{i-1}$ or $b_{i-1}$ , then $D$ answers with a set only containing the respective other node. In this case the follow-up position $(\{\{a_{i-1}\},\{b_{i-1}\}\},k-1)$ belongs to $W_{D}^{1}$ .

Lastly we look at the set $W_{D}^{8}$ . This set contains all positions $(\{\{6_{i}\},\{7_{i}\}\},k)$ with $i\geq 2$ and $k\leq 2^{i-1}-1$ . From such a position, $S$ may play an operator-move where he picks either $1_{i}$ or $a_{i-1}$ as a successor of $6_{i}$ or $2_{i}$ , $3_{i}$ or $b_{i-1}$ as a successor of $7_{i}$ . If he choose $1_{i}$ or $2_{i}$ , then $D$ answers with the respective other node as a singleton. The follow-up position $(\{\{1_{i}\},\{2_{i}\}\},k-1)$ is a member of $W_{D}^{4}$ . If $S$ choose $3_{i}$ instead, then $D$ answers with $\{1_{i}\}$ and the new position is $(\{\{1_{i}\},\{3_{i}\}\},k-1)$ , a member of $W_{D}^{5}$ . On the other hand if $S$ picked $a_{i-1}$ or $b_{i-1}$ , then $D$ picks $\{b_{i-1}\}$ and $\{a_{i-1}\}$ respectively. Then the game continues with $(\{\{a_{i-1}\},\{b_{i-1}\}\},k-1)$ , a position from $W_{D}^{1}$ . So all follow-up positions belong to $W_{D}$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Micah Adler and Neil Immerman. An $n!$ lower bound on formula size. ACM Transactions on Computational Logic, 4(3):296–314, 2003. doi:10.1145/772062.772064.

[bib.bib2] [2] Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Boolean basis, formula size, and number of modal operators. Logical Methods in Computer Science, Volume 21, Issue 3, July 2025. doi:10.46298/lmcs-21(3:10)2025.

[bib.bib3] [3] Marco Carmosino, Ronald Fagin, Neil Immerman, Phokion Kolaitis, Jonathan Lenchner, and Rik Sengupta. Multi-structural games and beyond. Logical Methods in Computer Scienc, 20:27:1–27:40, 2024. doi:10.48550/arXiv.2301.13329.

[bib.bib4] [4] Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129–141, 1960. URL: https://eudml.org/doc/213582.

[bib.bib5] [5] Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, and Nikhil Vyas. Multi-structural games and number of quantifiers. Logical Methods in Computer Science, 21(1), 2025. doi:10.46298/lmcs-21(1:10)2025.

[bib.bib6] [6] Roland Fraïssé. On some classifications of relationship systems. Publications scientifiques de l’Université d’Alger, Série A, Sciences mathématiques, 1954.

[bib.bib7] [7] Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. Succinctness of epistemic languages. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-11), pages 881–886, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-153.

[bib.bib8] [8] Martin Grohe and Nicole Schweikardt. The succinctness of first-order logic on linear orders. Logical Methods in Computer Science, 1(1), 2005. doi:10.2168/LMCS-1(1:6)2005.

[bib.bib9] [9] Lauri T. Hella and Miikka S. Vilander. Formula size games for modal logic and $\mu$ -calculus. Journal of Logic and Computation, 29(8):1311–1344, 2019. doi:10.1093/logcom/exz025.

[bib.bib10] [10] Vaughan R. Pratt. The effect of basis on size of boolean expressions. In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, pages 119–121, October 1975. doi:10.1109/SFCS.1975.29.

[bib.bib11] [11] Philip Spira. On time-hardware complexity tradeoffs for boolean functions. In Proceedings of the 4th Hawaii Symposium on System Sciences, 1971, pages 525–527, 1971.

[bib.bib12] [12] Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. On the relative succinctness of two extensions by definitions of multimodal logic. Lecture Notes in Computer Science, 7318 LNCS:323–333, 2012. doi:10.1007/978-3-642-30870-3_33.

[bib.bib13] [13] Hans van Ditmarsch, Jie Fan, Wiebe van der Hoek, and Petar Iliev. Some exponential lower bounds on formula-size in modal logic. In Advances in Modal Logic, volume 10, pages 139–157, August 2014. URL: https://www.scopus.com/inward/record.uri?eid=2-s2.0-84924671231&partnerID=40&md5=3f43caf649380733487e57e7338bd34d.

[bib.bib14] [14] Harry Vinall-Smeeth. From quantifier depth to quantifier number: Separating structures with $k$ variables. In Proceedings - Symposium on Logic in Computer Science, 2024. doi:10.1145/3661814.3662125.

Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

2.1 Modal logic with Bi-implication and Kripke structures

2.2 Formula size

3 The operator-number game

Definition 1.

Lemma 2.

Lemma 3.

Lemma 4.

Proof.

Lemma 5.

Proof.

Theorem 6.

4 Succinctness between ML[↔] and ML

Lemma 7.

Proof.

Claim 8.

Proof.

4.1 Transitive and reflexive graphs

Lemma 9.

Proof.

Lemma 10.

Proof.

Theorem 11.

Proof.

Corollary 12.

4.2 Symmetrical and reflexive graphs

Lemma 13.

Proof.

Lemma 14.

Proof.

Theorem 15.

Proof.

Corollary 16.

4.3 Transitive and symmetrical graphs

Theorem 17.

Proof.

5 Conclusion

References

Appendix A Appendix

A.1 Proof of Lemma 2

Proof.

A.2 Proof of Lemma 3

Proof.

A.3 Proof of Lemma 7

Proof.

A.4 Proof of Lemma 10

Proof.

A.5 Proof of Lemma 14

Proof.

4 Succinctness between ML[ $\leftrightarrow$ ] and ML