An expressive completeness theorem for coalgebraic modal mu-calculi

TL;DR

This paper establishes a coalgebraic modal mu-calculus completeness theorem by linking it to monadic second-order logic invariance, using automata-theoretic methods to generalize classical results across various functors.

Contribution

It introduces an adequate uniform construction for coalgebraic functors, enabling a broad characterization of the coalgebraic mu-calculus as the bisimulation-invariant fragment of MSO logic.

Findings

Provides a new proof of the Janin-Walukiewicz Theorem for modal mu-calculus

Establishes bisimulation invariance for the bag functor and exponential polynomial functors

Derives a characterization theorem for the monotone modal mu-calculus

Abstract

Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the "game functor"). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.

Figures

Tables

Table 1. Table 1. Acceptance game for 𝙼𝚂𝙾 𝙼𝚂𝙾 \mathtt{MSO} -automata

Position	Player	Admissible moves	Priority
$(a,s)\in A\times S$	$\exists$	$\{U:A\to 𝒫\left(R\left[s\right]\right)\mid (R\left[s\right],U)⊩\Delta (a,V^{†}\left(s\right))\}$	$\Omega \left(a\right)$
$U:A\to 𝒫S$	$\forall$	$\{(b,t)\mid t\in U\left(b\right)\}$	$0$

Table 2. Table 2. Acceptance game for modal automata

Position	Player	Admissible moves	Priority
$(a,s)\in A\times S$	$\exists$	$\{U\in {\left(𝒫S\right)}^A\mid (S,\sigma \left(s\right),U){⊩}_1\Delta (a,V^{†}\left(s\right))\}$	$\Omega \left(a\right)$
$U:A\to 𝒫S$	$\forall$	$\{(b,t)\mid t\in U\left(b\right)\}$	$0$

Table 3. Table 3. Acceptance game for 𝙻 𝙻 \mathtt{L} -automata.

Position	Player	Admissible moves	Priority
$(a,s)\in A\times T$	$\exists$	$\{U:A\to 𝒫\left(R\left(s\right)\right)\mid (R\left(s\right),\sigma \left(s\right){|}_{R\left(s\right)},U){⊩}_1\Delta (a,V^{†}\left(s\right))\}$	$\Omega \left(a\right)$
$U:A\to 𝒫\left(T\right)$	$\forall$	$\{(b,t)\mid t\in U\left(b\right)\}$	$0$

Table 4. Table 4. The extended acceptance game

Position	Player	Admissible moves	Priority
$({\psi }_1\vee {\psi }_2,s)$	$\exists$	$\{({\psi }_1,s),({\psi }_2,s)\}$	$0$
$({\psi }_1\wedge {\psi }_2,s)$	$\forall$	$\{({\psi }_1,s),({\psi }_2,s)\}$	$0$
$(a,s)\in A\times S$	$\exists$	$\left\{(\Delta (a,V^{†}\left(s\right)),s)\right\}$	$\Omega \left(a\right)$
$(\lambda ({\psi }_1,\dots ,{\psi }_n),s)$	$\exists$	$\{f:\mathrm{𝙻𝚊𝚝𝚝}\left(A\right)\to 𝒫S\mid \sigma \left(s\right)\in \lambda (f\left({\psi }_1\right),\dots ,f\left({\psi }_n\right))\}$	$0$
$(\top ,s)$	$\forall$	$\varnothing$	$0$
$(\perp ,s)$	$\exists$	$\varnothing$	$0$
$f:\mathrm{𝙻𝚊𝚝𝚝}\left(A\right)\to 𝒫\left(S\right)$	$\forall$	$\{(\psi ,s)\mid s\in f\left(\psi \right)\}$	$0$

Equations

$$\mathbb{A}\text{ accepts }({\mathbb{S}}_{\ast },s_{\ast })\text{ iff }{\mathbb{A}}^{\ast }\text{ accepts }(\mathbb{S},s).$$

$${\mathtt{MSO}}_{\mathsf{T}}/\sim \equiv \mu {\mathtt{ML}}_{\mathsf{T}}.$$

$$(A,\Delta ,a_I,F)$$

$$F^{\prime }=\{B\subseteq A\mid B\cap F\ne \varnothing \}$$

$${\Delta }^{\prime }(B,c)=\bigcup \{\Delta (b,c)\mid b\in B\}.$$

$$B_{\Pi }^{+}=\{\pi \in B_{\Pi }\mid E[\pi ]\ne \varnothing \}.$$

$$\phi ::=\mathsf{sr}(p)|p\subseteq q|R(p,q)|\neg \phi |\phi \vee \phi |\exists p.\phi$$

$$\phi ::=p|\neg p|\phi \vee \phi |\phi \wedge \phi |\square \phi |◊\phi |\eta p.\phi$$

$$\mu \mathtt{ML}\equiv \mathtt{MSO}/\sim$$

$$a(x)\mid x=y\mid \phi \wedge \phi \mid \neg \phi \mid \exists x.\phi$$

$$\Delta :A\times \mathcal{P}(P)\to {\mathtt{FOE}}^{+}(A)$$

$$(a_0,s_0)U_0(a_1,s_1)U_1...U_{n-1}(a_n,s_n)$$

$$(a_0,s_0)....(a_n,s_n)$$

$$\exists x_1...\exists x_n(\mathsf{diff}(x_1,...,x_n)\wedge a_1(x_1)\wedge ...\wedge a_n(x_n)\wedge \forall y(\mathsf{diff}(x_1,...,x_n,y)\to b_1(y)\vee ...\vee b_k(y)))$$

$$\underset{1\le i<j\le m}{\bigwedge }\neg (z_i=z_j)$$

$${\sigma }_2\circ f=\mathsf{T}f\circ {\sigma }_1.$$

$$\{N\in \mathcal{QQ}X\mid \forall Z,Z^{\prime }:Z\in N\&Z\subseteq Z^{\prime }\Rightarrow Z^{\prime }\in N\}.$$

$$(\alpha ,\beta )\in \overline{\mathcal{P}}(R)\iff (\forall x\in \alpha \exists y\in \beta :xRy)\&(\forall y\in \beta \exists x\in \alpha :xRy)$$

$$R=\{(u,v)\in X_1\times X_2\mid f_1(u)=f_2(v)\}$$

$$\overline{\mathsf{T}}R:=\{({\alpha }_1,{\alpha }_2)\in \mathsf{T}{X}_1\times \mathsf{T}{X}_2\mid \exists \gamma \in \mathsf{T}R:\mathsf{T}{\pi }_1(\gamma )=\alpha \&\mathsf{T}{\pi }_2(\gamma )={\alpha }_2\}$$

$$\lambda :{\mathcal{Q}}^n\to \mathcal{Q}\circ \mathsf{T},$$

$${\lambda }_X(Y_1,...,Y_n)\subseteq {\lambda }_X(Z_1,...,Z_n),$$

$$(Z_1,...,Z_n)\mapsto \mathsf{T}X\setminus ({\lambda }_X(X\setminus Z_1,...,X\setminus Z_n)).$$

$$\phi ::=p|\neg p|\lambda ({\phi }_1,...,{\phi }_n)|{\lambda }^d({\phi }_1,...,{\phi }_n)|\phi \vee \phi |\phi \wedge \phi |\eta p.\phi$$

$$\alpha \in {◊}_X(Z)\iff \alpha \cap Z\ne \varnothing$$

$$\alpha \in {\square }_X(Z)\iff Z\in \alpha$$

$$\phi ::=\perp |\top |\lambda ({\psi }_1,...,{\psi }_n)|{\lambda }^d({\psi }_1,...,{\psi }_n)|\phi \vee \phi |\phi \wedge \phi$$

$$\perp |\top |a|\phi \vee \phi |\phi \wedge \phi$$

$$(X,\alpha ,\mathcal{Q}f\circ V){⊩}_1\lambda \iff (Y,\mathsf{T}f(\alpha ),V){⊩}_1\lambda .$$

$$\Delta :A\times \mathcal{P}(P)\to {1ML}_{\Lambda }(A)$$

Full text

Fatemeh Seifan was supported by Vrije Competitie grant 612.001.115 of the Netherlands Organisation for Scientific Research (NWO)

1. Introduction

1.1. Logic, automata and coalgebra

The aim of this paper is to strengthen the link between the areas of logic, automata and coalgebra. More precisely, we provide a coalgebraic generalization of the automata-theoretic approach towards monadic second-order logic ($\mathtt{MSO}$), and we address the question of whether the Janin-Walukiewicz Theorem can be generalized from Kripke structures to the setting of arbitrary coalgebras111The paper is a substantially extended version of a previous manuscript that was presented at the 2015 conference for Logic in Computer Science (LICS 2015) in Kyoto, Japan [7]..

The connection between monadic second-order logic and automata is classic, going back to the seminal work of Büchi, Rabin, and others. Rabin’s decidability result for the monadic second-order theory of binary trees, or $S2S$, makes use of a translation of monadic second-order logic into a class of automata, thus reducing the satisfiability problem for $S2S$ to the non-emptiness problem for the corresponding automata [28]. The link between $\mathtt{MSO}$ and automata over trees with arbitrary branching was further explored by Walukiewicz [36]. Janin and Walukiewicz considered monadic second-order logic interpreted over Kripke structures, and used automata-theoretic techniques to obtain a van Benthem-like characterization theorem for monadic second-order logic, identifying the modal $\mu$-calculus as the bisimulation invariant fragment of $\mathtt{MSO}$ [13]. Given the fact that in many applications bisimilar models are considered to represent the same process, one has little interest in properties of models that are not bisimulation invariant. Thus the Janin-Walukiewicz Theorem can be seen as an expressive completeness result, stating that all relevant properties in monadic second-order logic can be expressed in the modal $\mu$-calculus.

Coalgebra enters naturally into this picture. Recall that Universal Coalgebra [29] provides the notion of a coalgebra as the natural mathematical generalization of state-based evolving systems such as streams, (infinite) trees, Kripke models, (probabilistic) transition systems, and many others. This approach combines simplicity with generality and wide applicability: many features, including input, output, nondeterminism, probability, and interaction, can easily be encoded in the coalgebra type $\mathsf{T}$ (formally an endofunctor on the category $\mathbf{Set}$ of sets as objects with functions as arrows). Starting with Moss’ seminal paper [23], coalgebraic logics have been developed for the purpose of specifying and reasoning about behavior, one of the most fundamental concepts that allows for a natural coalgebraic formalization. And with Kripke structures constituting key examples of coalgebras, it should come as no surprise that most coalgebraic logics are some kind of modification or generalization of modal logic [5].

The coalgebraic modal logics that we consider here originate with Pattinson [27]; they are characterized by a completely standard syntax, in which the semantics of each modality is determined by a so-called predicate lifting (see Definition 3.2 below). Many well-known variations of modal logic in fact arise as the coalgebraic logic associated with a set $\Lambda$ of such predicate liftings; examples include both standard and (monotone) neighborhood modal logic, graded and probabilistic modal logic, coalition logic, and conditional logic. Extensions of coalgebraic modal logics with fixpoint operators, needed for describing ongoing behavior, were developed in [33, 4].

The link between coalgebra and automata theory is by now well-established. For instance, finite state automata operating on finite words have been recognized as key examples of coalgebra from the outset [29]. More relevant for the purpose of this paper is the link with precisely the kind of automata mentioned earlier, since the (potentially infinite) objects on which these devices operate, such as streams, trees and Kripke frames, usually are coalgebras. Thus, the automata-theoretic perspective on modal fixpoint logic may be lifted to the abstraction level of coalgebra [33, 8]. In fact, many key results in the theory of automata operating on infinite objects, such as Muller & Schupp’s Simulation Theorem [25] can in fact be seen as instances of more general theorems in Universal Coalgebra [15].

1.2. Coalgebraic monadic second-order logic

Missing from this picture is, to start with, a coalgebraic version of (monadic) second-order logic. Filling this gap is the first aim of the current paper, which introduces a notion of monadic second-order logic $\mathtt{MSO}_{\mathsf{T}}$ for coalgebras of type $\mathsf{T}$. Our formalism combines two ideas from the literature. First of all, we looked for inspiration to the coalgebraic versions of first-order logic of Litak & alii [17]. These authors introduced Coalgebraic Predicate Logic as a common generalisation of first-order logic and coalgebraic modal logic, combining first-order quantification with coalgebraic syntax based on predicate liftings. Our formalism $\mathtt{MSO}_{\mathsf{T}}$ will combine a similar syntactic feature with second-order quantification. In fact it can be shown to contain the Coalgebraic Predicate Logic of Litak & alii as a fragment, though we will omit the verification of this fact.

Second, following the tradition in automata-theoretic approaches towards monadic second-order logic, our formalism will be one-sorted. That is, we only allow second-order quantification in our language, relying on the fact that individual quantification, when called for, can be encoded as second-order quantification relativized to singleton sets. Since predicate liftings are defined as families of maps on powerset algebras, these two ideas fit together very well, to the effect that our second-order logic is in some sense simpler than the first-order formalism of [17].

In section 4 we will define, for any set $\Lambda$ of monotone222In the most general case, restricting to monotone predicate liftings is not needed, one could define $\mathtt{MSO}_{\mathsf{T}}$ as the logic obtained by taking for $\Lambda$ the set of all predicate liftings. However, in the context of this paper, where we take an automata-theoretic perspective on $\mathtt{MSO}$, this restriction makes sense.

predicate liftings, a formalism $\mathtt{MSO}_{\Lambda}$, and we let $\mathtt{MSO}_{\mathsf{T}}$ denote the logic obtained by taking for $\Lambda$ the set of all monotone predicate liftings. Clearly we will make sure that this definition generalizes the standard case, in the sense that the standard version of $\mathtt{MSO}$ for Kripke structures instantiates the logic $\mathtt{MSO}_{\{\Diamond\}}$ and is equivalent to the coalgebraic logic $\mathtt{MSO}_{\mathcal{P}}$ (where $\mathcal{P}$ denotes the power set functor).

The introduction of a monadic second-order logic $\mathtt{MSO}_{\mathsf{T}}$ for $\mathsf{T}$-coalgebras naturally raises the question, for which $\mathsf{T}$ does the coalgebraic modal $\mu$-calculus for $\mathsf{T}$, denoted $\mathtt{\mu ML}_{\mathsf{T}}$, correspond to the bisimulation-invariant fragment of $\mathtt{MSO}_{\mathsf{T}}$.

{qu}

Which functors $\mathsf{T}$ satisfy $\mathtt{\mu ML}_{\mathsf{T}}\equiv\mathtt{MSO}_{\mathsf{T}}/{\sim}$?

1.3. Automata for coalgebraic monadic second-order logic

In order to address Question 1.2, we take an automata-theoretic perspective on the logics $\mathtt{MSO}_{\mathsf{T}}$ and $\mathtt{\mu ML}_{\mathsf{T}}$, and as the second contribution of this paper we introduce a class of parity automata for $\mathtt{MSO}_{\mathsf{T}}$.

As usual, the operational semantics of our automata is given in terms of a two-player acceptance game, which proceeds in rounds moving from one basic position to another, where a basic position is a pair consisting of a state of the automaton and a point in the coalgebra structure under consideration. In each round, the two players, $\exists$ and $\forall$, focus on a certain local ‘window’ on the coalgebra structure. This ‘window’ takes the shape of a one-step $\mathsf{T}$-model, that is, a triple $(X,\alpha,V)$ consisting of a set $X$, a chosen object $\alpha\in\mathsf{T}X$ (representing partial information about the transition map of the coalgebra as seen from the perspective of some given state), and a valuation $V$ interpreting the states of the automaton as subsets of $X$. More specifically, during each round of the game it is the task of $\exists$ to come up with a valuation $V$ that creates a one-step model in which a certain one-step formula $\delta$ (determined by the current basic position in the game) is true.

Generally, our automata will have the shape $\mathbb{A}=(A,\Delta,\Omega,a_{I})$ where $A$ is a finite carrier set with initial state $a_{I}\in A$, and $\Omega$ and $\Delta$ are the parity and transition map of $\mathbb{A}$, respectively. The flavour of such an automaton is largely determined by the co-domain of its transition map $\Delta$, the so-called one-step language which consists of the one-step formulas that feature in the acceptance game as described.

Each one-step language $\mathtt{L}$ induces its own class of automata $\mathit{Aut}(\mathtt{L})$. For instance, the class of automata corresponding to the coalgebraic fixpoint logic $\mathtt{\mu ML}_{\Lambda}$ can be given as $\mathit{Aut}(\mathtt{ML}_{\Lambda})$, where $\mathtt{ML}_{\Lambda}$ is the set of positive modal formulas of depth one that use modalities from $\Lambda$ [8]. Basically then, the problem of finding the right class of automata for the coalgebraic monadic second-order logic $\mathtt{MSO}_{\Lambda}$ consists in the identification of an appropriate one-step language. Our proposal comprises a one-step second-order logic $\mathtt{SO}_{\Lambda}$ which uses predicate liftings to describe the chosen object of the one-step model.

Finally, note that similar to the case of standard $\mathtt{MSO}$, the equivalence between formulas in $\mathtt{MSO}_{\mathsf{T}}$ and automata in $\mathit{Aut}(\mathtt{SO}_{\Lambda})$ is only guaranteed to hold for coalgebras that are ‘tree-like’ in some sense (to be defined further on).

Theorem 1** (Automata for coalgebraic $\mathtt{MSO}$).**

For any set $\Lambda$ of monotone predicate liftings for $\mathsf{T}$ there is an effective construction mapping any formula $\varphi\in\mathtt{MSO}_{\Lambda}$ into an automaton $\mathbb{A}_{\varphi}\in\mathit{Aut}(\mathtt{SO}_{\Lambda})$, which is equivalent to $\varphi$ over $\mathsf{T}$-tree models.

The proof of Theorem 1 proceeds by induction on the complexity of $\mathtt{MSO}_{\mathsf{T}}$-formulas, and thus involves various closure properties of automata, such as closure under complementation, union and projection. In order to establish these results, it will be convenient to take an abstract perspective revealing how closure properties of a class of automata are completely determined at the level of the one-step language, similar to the development in [36].

1.4. Bisimulation Invariance

With automata-theoretic characterizations in place for both coalgebraic $\mathtt{MSO}$ and the coalgebraic $\mu$-calculus $\mathtt{\mu ML}$, we can address Question 1.2 by considering the following question: {qu}

Which functors $\mathsf{T}$ satisfy $\mathit{Aut}(\mathtt{ML}_{\mathsf{T}})\equiv\mathit{Aut}(\mathtt{SO}_{\mathsf{T}})/{\sim}$?

Continuing the program of the third author [35], we will approach this question at the level of the one-step languages, $\mathtt{SO}$ and $\mathtt{ML}$. To start with, observe that any translation (from one-step formulas in) $\mathtt{SO}$ to (one-step formulas in) $\mathtt{ML}$ naturally induces a translation from $\mathtt{SO}$-automata to $\mathtt{ML}$-automata. A new observation we make here is that any so-called uniform construction on the class of one-step models for the functor $\mathsf{T}$ that satisfies certain adequacy conditions, provides (1) a translation $(\cdot)^{*}:\mathtt{SO}\to\mathtt{ML}$, together with (2) a construction $(\cdot)_{*}$ transforming a pointed $\mathsf{T}$-model $(\mathbb{S},s)$ into a tree model $(\mathbb{S}_{*},s_{*})$ which is a coalgebraic pre-image of $(\mathbb{S},s)$ satisfying

[TABLE]

where $\mathbb{A}^{*}$ is obtained by applying to $\mathbb{A}$ the lifting of the one-step translation $(\cdot)^{*}:\mathtt{SO}\to\mathtt{ML}$ to the level of automata. From this it easily follows that an $\mathtt{SO}$-automaton $\mathbb{A}$ is bisimulation invariant iff it is equivalent to the $\mathtt{ML}$-automaton $\mathbb{A}^{*}$.

On the basis of these observations we can prove the following generalisation of the Janin-Walukiewicz Theorem.

Theorem 2** (Coalgebraic Bisimulation Invariance).**

Let $\mathsf{T}$ be any set functor. If $\mathsf{T}$ admits an adequate uniform construction for every finite set of second-order one-step formulas $\Gamma$, then

[TABLE]

In our view, the proof of this theorem separates the ‘clean’, abstract part of bisimulation-invariance results from the more functor-specific parts. As a consequence, Theorem 2 can be used to obtain immediate results in particular cases. Examples include the power set functor (standard Kripke structures), where the adequate uniform construction roughly consists of taking $\omega$-fold products (see Example 5.3), the bag functor (Example 5.3), and all exponential polynomial functors (Corollary 37).

However, it turns out that there are cases of functors that provably do not admit an adequate uniform construction. A concrete example is the monotone neighborhood functor $\mathcal{M}$ (see the next section for its definition), which provides the semantics for monotone modal logic  [10] and its fixpoint extension, the monotone $\mu$-calculus. The monotone $\mu$-calculus is interesting for at least two reasons: first, it has a purely theoretical interest as a natural candidate for a minimal modal $\mu$-calculus, since the only constraint on the box operator is monotonicity rather than the stronger constraint of complete multiplicativity of the box operator in normal modal logic. In other words, the base modal logic has precisely the logical strength it needs so that Knaster-Tarski-style extremal fixpoints may be smoothly introduced, and no more. Second, a more application driven reason to study the monotone $\mu$-calculus is that it is the natural fixpoint logic in which Parikh’s dynamic logic of games [26] sits as a fragment in the same manner that PDL is a fragment of the modal $\mu$-calculus. (More precisely, game logic is a fragment of a multi-modal variant of the monotone modal $\mu$-calculus, but we will stick to the monomodal case for the sake of notational convenience.) As the final contribution of this paper we show how, with some extra work, a characterization result for the monotone $\mu$-calculus can be derived using our main result 2, with respect to a natural monadic second-order language for monotone neighborhood structures that we call “monotone MSO”.

Theorem 3**.**

The monotone $\mu$-calculus is the fragment of monotone MSO that is invariant for neighborhood bisimulations.

2. Some technical background

In this section we provide some of the necessary technical background. We shall assume familiarity with coalgebras, and at least some basic acquaintance with modal logic and the modal $\mu$-calculus. We will provide insofar as possible a self-contained presentation of the required material on automata and infinite games.

2.1. Automata

Throughout most of its history, the mathematical theory surrounding the modal $\mu$-calculus has relied heavily on the theory of automata operating on infinite objects and, what is closely related, infinite games. It turns out that these frameworks fit nicely into the coalgebraic world view, which is to be expected as infinite games and automata operating on infinite objects both have a coinductive flavour. This connection is in fact a big part of what makes the coalgebraic modal $\mu$-calculus tick, and will be central to this paper. In this section we give a brief overview of this field. The material that we cover is entirely standard, so readers who are already familiar with these topics will want to merely skim the section to fix notation and terminology.

We start with something that probably most readers have already come across at some point: the theory of word automata recognizing regular languages over some alphabet. (For an introduction to the basic concepts of automata theory, see [11].) {defi} A (non-deterministic) word automaton is a tuple:

[TABLE]

where $A$ is a finite set, $\Delta:A\times\Sigma\to\mathcal{P}(A)$, $a_{I}\in A$ and $F\subseteq A$.

The general mold into which many types of automata fit is of this shape: they consist of a set of states ($A$), a *transition structure * ($\Delta$) telling us how to move between states of the automaton, an initial state ($a_{I}$) and, finally, some data structure over $A$ that lets us know whether or not a given computation carried out by an automaton accepts or rejects its input. In the case of word automata, the input $\vec{w}$ of an automaton is a finite word $c_{0}....c_{n}$ over the alphabet $\Sigma$ (i.e. an element of $\Sigma^{n}$ for some $n$). {defi} A run of the automaton $\mathbb{A}$ on a word $\vec{w}$ is a tuple $a_{0}....a_{n+1}$ of states in $A$, such that $a_{0}=a_{I}$ and $a_{i+1}\in\Delta(a_{i},c_{i})$ for $i\leq n$. The run is said to be accepting if $a_{n+1}\in F$, and we say that $\mathbb{A}$ accepts the word $\vec{w}$ if there is some accepting run of $\mathbb{A}$ on the input $\vec{w}$. The language $L(\mathbb{A})$ of an automaton $\mathbb{A}$ is simply the collection of all the words that it accepts.

A central technique in automata theory is to show that one can simplify the transition structure of some class of automata, without losing any expressive power. In the case of word automata, it is well known that the non-deterministic automata that we have defined here have the same expressive power as deterministic word automata, which are defined as ones that satisfy the condition that $\Delta(a,c)$ is a singleton for each $a\in A$. This means that there is a unique run of the automaton on every input.

Fact 4** (Simulation of word automata).**

For every word automaton $\mathbb{A}$, there exists a deterministic word automaton $\mathbb{A}^{\prime}$ with $L(\mathbb{A})=L(\mathbb{A}^{\prime})$.

The proof consists of an elegant construction known as the powerset construction: given an automaton $\mathbb{A}=(A,\Delta,a_{I},F)$, we construct a deterministic automaton $\mathbb{A}^{\prime}=(A^{\prime},\Delta^{\prime},a_{I}^{\prime},F^{\prime})$ recognizing the same language by setting $A^{\prime}=\mathcal{P}(A)$, $a_{I}^{\prime}=\{a_{I}\}$, the accepting states are defined by

[TABLE]

and the transition structure is defined

[TABLE]

Intuitively, the states of $\mathbb{A}^{\prime}$ consist of “macro-states” over $\mathbb{A}$, consisting of several states of $\mathbb{A}$ being visited at once, and a run of $\mathbb{A}^{\prime}$ on a word can be viewed as a “bundle” of runs of $\mathbb{A}$ on the same word. These sorts of simulation theorems turn up in various places, for various types of automata. In particular, one of our main technical results of this paper is a simulation theorem, allowing us to simplify the transition structure of the automata that we introduce for monadic second-order logic interpreted on coalgebras.

In this paper we are mainly interested in automata that, unlike word automata, classify infinite objects. The simplest non-trivial example of this is the theory of automata operating on infinite words, or streams as we shall call them. For a given alphabet $\Sigma$, a $\Sigma$-stream is an $\omega$-sequence of elements of $\Sigma$. Automata that are used to classify streams are called stream automata. The simplest kind of stream automata, known as Büchi automata, are simply the same as word automata: they consist of a set of states $A$, a transition relation $\Delta:A\times\Sigma\to\mathcal{P}(A)$, a start state $a_{I}$ and a set $F$ of accepting states. The difference is in the definition of acceptance. {defi} Given a stream $c_{0}c_{1}c_{2}c_{3}...$ over $\Sigma$, a run of the automaton $\mathbb{A}$ is a stream $a_{0}a_{1}a_{2}a_{3}...$ over $A$, such that $a_{0}=a_{I}$ and $a_{i+1}\in\Delta(a_{i},c_{i})$ for all $i<\omega$. The run is said to be accepting if the following acceptance condition is met: for infinitely many $i\in I$, we have $a_{i}\in F$.

In other words, a run is accepting if from each given point in the computation, the automaton will eventually end up in an accepting state. The language $L(\mathbb{A})$ consists of the set of $\Sigma$-streams accepted by $\mathbb{A}$.

Again, one of the central results about stream automata is a simulation theorem. However, here the Büchi condition is not flexible enough - it is a standard fact that deterministic Büchi automata have strictly less expressive power than non-deterministic ones. To obtain a simulation theorem, we need to switch to a more sophisticated acceptance condition, and several are available (see [34] for an overview). For the purposes of the present paper, the most natural condition is the parity condition.

Given a finite set $A$, a priority map is simply a map $\Omega:A\to\omega$, assigning a natural number to each element of $A$. Such a map encodes, in a compact way, two pieces of information that we want to keep track of: first, it partitions the states in $A$ into two sets, the states with even priority and the ones with odd priority. Intuitively, think of the states with even priority as the accepting states. Second, the priority map encodes an ordering of the states, where states of higher priority are regarded as more important when determining whether or not a run is accepting. A parity stream automaton is then a tuple $(A,\Delta,a_{I},\Omega)$, where $\Omega$ is a priority map. A run $a_{0}a_{1}a_{2}...$ on some stream is now said to be accepting if the highest number $k$ such that $\Omega(a_{i})=k$ for infinitely many $i$ is an even number. In other words: the run visits some accepting state $a$ infinitely many times, and any non-accepting state that is also visited infinitely many times has lower priority than $a$.

Switching from Büchi automata to parity automata does not give any more expressive power: the two automaton models are expressively equivalent. The point of the parity condition is that we now have a simulation theorem available:

Fact 5** (Simulation of stream automata).**

For every parity stream automaton $\mathbb{A}$, there is a deterministic parity stream automaton $\mathbb{A}^{\prime}$ (i.e. such that $\Delta^{\prime}(a^{\prime},c)$ is a singleton for all $a^{\prime}\in A^{\prime}$) with $L(\mathbb{A})=L(\mathbb{A}^{\prime})$.

A standard proof of this simulation theorem for stream automata uses a construction due to Safra, which is quite involved compared to the powerset construction for word automata. We refer to [34] for the details.

Simulation theorems are particularly useful for proving closure properties of automata; for example, given a deterministic parity stream automaton $\mathbb{A}$, it is trivial to define its complement, i.e. an automaton that accepts all and only those streams that are not accepted by $\mathbb{A}$. The construction just adjusts the priority map: if $\Omega$ was the priority map of $\mathbb{A}$, then define the complement of $\mathbb{A}$ to be just like $\mathbb{A}$ but with the priority map $\Omega^{\prime}$ defined by $\Omega^{\prime}(a)=\Omega(a)+1$.

2.2. Infinite games

The automata we considered in the previous section are all of a fairly simple character: when processing a word or a stream, these automata simply change their state depending on the input that they read, in a deterministic or non-deterministic manner, and the sequence of states visited in this manner is what we have called a run. For more complex automaton models, this notion of a “run” of the automaton on some input will no longer be adequate - more elaborate models of computation will be required. Here, the theory of infinite games has turned out be a powerful mathematical framework, providing simple and perspicious models of how automata process their input. The idea is to think of the computation carried out by an automaton as a game between two players with opposite goals: one player tries to defend the view that the input should be accepted, the other tries to show that it should be rejected. {defi} A board game $\mathbb{G}$ is a tuple $(B_{\exists},B_{\forall},E,W)$ where $B_{\exists}$ and $B_{\forall}$ are disjoint sets, $E\subseteq B\times B$ where $B=B_{\exists}\cup B_{\forall}$ (this union is called the board) and $W$ is a map from the set $B^{\omega}$ of $B$-streams into the set $\{\exists,\forall\}$. Elements of $B$ are called positions.

Intuitively, $\exists$ (or Eloise) and $\forall$ (or Abelard) are the players, $B_{\exists}$ consists of the positions on the board at which it is $\exists$’s turn to move, and similarly for $B_{\forall}$. Finally, the relation $E$ tells us what the legal moves are at a given position of the game. It can happen that there are no legal moves at all at a position of the game.

There is nothing to prevent that a match of a board game could go on indefinitely. In fact this is crucial to the connection between infinite games and automata operating on non-wellfounded structures, in which the computation carried out by the automaton processing some input can be infinitely long. In these cases, the map $W$ will be used to decide a winner. Formally: {defi} Let $\mathbb{G}=(B_{\exists},B_{\forall},E,W)$ be any board game. A match in $\mathbb{G}$ is either a finite tuple of positions $\pi_{0}...\pi_{n}$ or an infinite sequence $\pi_{0}\pi_{1}\pi_{2}...$ of positions in $B$, such that $a_{i}Ea_{i+1}$ for all $i\in\omega$ (or for all $i<n$, if the match is finite.) A match $\rho$ is called complete if it is infinite, or if $E[\pi]=\{\pi^{\prime}\mid\pi E\pi^{\prime}\}=\emptyset$ where $\pi$ is the last position on $\rho$. If $\rho$ is not complete it is called a partial match. The set of partial matches $\rho$ of $\mathbb{G}$ for which the last position $\pi$ of $\rho$ belongs to $\Pi$, and such that $E[\pi]\neq\emptyset$, is denoted by $\mathsf{PM}(\mathbb{G},\Pi)$. The winner of an infinite match $\rho$ is defined to be $W(\rho)$, and the winner of a complete but finite match is $\exists$ if the last position is in $B_{\forall}$, and $\forall$ if the last position of the match is in $B_{\exists}$. In these cases, we say that the losing player got stuck.

{defi}

A strategy for a player $\Pi$ in a board game $\mathbb{G}$ is a map $\chi:\mathsf{PM}(\mathbb{G},\Pi)\to B$. A match $\rho$ (complete or partial) is said to be $\chi$-guided if, for every proper initial segment $\rho^{\prime}$ of $\rho$ that belongs to $\mathsf{PM}(\mathbb{G},\Pi)$, the tuple $\rho^{\prime}\chi(\rho^{\prime})$ is also an initial segment of $\rho$.

Finally, a strategy $\chi$ for $\Pi$ is said to be a winning strategy at a position $\pi$ in $\mathbb{G}$ if every $\chi$-guided match beginning with the position $\pi$ is won by $\Pi$. If there is a winning strategy for $\Pi$ at the position $\pi$ then we say that $\pi$ is a winning position for $\Pi$.

Remark 6**.**

The reader may be more familiar with a different terminology here, where the word “play” is used for what we call a “match”, and a play is said to “respect the strategy $\chi$” if it is $\chi$-guided in our sense.

In practice, when we define a winning strategy $\chi$ for either player in a game $\mathbb{G}$ for some given position $\pi$, we will usually only take care to define the strategy on those partial matches that are actually reachable from the position $\pi$ by a $\chi$-guided match.

A special role in connection with automata is played by parity games, where the winning condition $W$ is defined via a map $\Omega:B\to\omega$, such that the range $\Omega[B]$ of this map is finite. We then set $W(\rho)=\exists$ if the highest natural number $k$ such that $\Omega(\pi_{i})=k$ for infinitely many $i\in\omega$ is an even number, and we set $W(\rho)=\forall$ otherwise. It follows straightforwardly from a classic result in the theory of infinite games, the Borel determinacy theorem [18], that all parity games are determined, meaning that the winning positions for $\exists$ and $\forall$ partition the board: every position is winning for one of the two players. However, a much stronger and quite useful property holds for parity games: {defi} A strategy $\chi$ for $\Pi$ is said to be positional if, for any two partial matches $\rho_{1},\rho_{2}\in\mathsf{PM}(\mathbb{G},\Pi)$ such that the last positions of $\rho_{1}$ and $\rho_{2}$ are identical, we have $\chi(\rho_{1})=\chi(\rho_{2})$.

A positional strategy for $\Pi$ can thus be represented equivalently as a map $\chi:B_{\Pi}^{+}\to B$, where

[TABLE]

Fact 7** (Positional Determinacy).**

Let $\mathbb{G}$ be a parity game. Then for every position $\pi\in B$, there exists a unique player $\Pi\in\{\exists,\forall\}$ and a positional winning strategy for $\Pi$ at the position $\pi$.

Several proofs of the positional determinacy theorem are known, see [6, 24, 37]. We will briefly consider games with non-parity winning condition later; however, all the games we consider will be determined (although not necessarily by positional strategies), as an easy consequence of the Borel determinacy theorem.

2.3. Logics for Kripke models and their automata

With the required machinery in place, we are ready to explain the connection between infinite games, automata, monadic second-order logic and the modal $\mu$-calculus.

Let us start by briefly reviewing monadic second-order logic and the modal $\mu$-calculus, viewed as languages for reasoning about Kripke models. For simplicity we restrict our attention to Kripke models with just one accessibility relation, i.e. models for modal logic in the basic similarity type with just one diamond and one box. Let $\mathit{Var}$ be a fixed infinite supply of variables. {defi} A Kripke model is a structure $\mathbb{S}=(S,R,V)$ where $S$ is a set, $R\subseteq S\times S$ and $V:\mathit{Var}\rightarrow\mathcal{P}(S)$ is a $\mathit{Var}$-valuation. A pointed Kripke model is a structure $(\mathbb{S},s)$ where $\mathbb{S}$ is a Kripke model and $s$ is a point in $\mathbb{S}$.

Associated with a valuation $V$, we define the conjugate coloring $V^{\dagger}:S\to\mathcal{P}(\mathit{Var})$ by $V^{\dagger}(s)\mathrel{:=}\{p\in\mathit{Var}\mid s\in V(p)\}$. Given a subset $Z\subseteq S$, the valuation $V[p\mapsto Z]$ is as $V$ except that it maps the variable $p$ to $Z$.

Turning to syntax, we define the formulas of monadic second-order logic $\mathtt{MSO}$ through the following grammar:

[TABLE]

with $p,q\in\mathit{Var}$. (Here, $\mathsf{sr}$ stands for “source”.) We define $\top:=\forall p.p\subseteq p$ and $\bot:=\neg\top$. Formulas are evaluated over pointed Kripke models by the following induction:

• •

$(S,R,V,s)\Vdash\mathsf{sr}(p)$ iff $V(p)=\{s\}$

• •

$(S,R,V,s)\Vdash p\subseteq q$ iff $V(p)\subseteq V(q)$

• •

$(S,R,V,s)\Vdash R(p,q)$ iff for all $v\in V(p)$ there is $w\in V(q)$ with $vRw$

• •

standard clauses for the boolean connectives

• •

$(S,R,V,s)\Vdash\exists p.\varphi$ iff $(S,R,V[p\mapsto Z],s)\Vdash\varphi$ for some $Z\subseteq S$.

We present the language of the modal $\mu$-calculus $\mathtt{\mu ML}$ in negation normal form, by the following grammar:

[TABLE]

where $p\in\mathit{Var}$, $\eta\in\{\mu,\nu\}$, and in the formula $\eta p.\varphi$ no free occurrence of the variable $p$ in $\varphi$ may be in the scope of a negation. We define $\top:=\nu p.p$ and $\bot:=\mu p.p$.

The satisfaction relation between pointed Kripke models and formulas in $\mathtt{\mu ML}$ is defined by the usual induction, with, e.g.

• •

$(S,R,V,s)\Vdash\mu p.\varphi$ iff $s\in\bigcap\{Z\subseteq S\mid\varphi_{p}(Z)\subseteq Z\}$ where $\varphi_{p}(Z)$ denotes the truth set of the formula $\varphi$ in the model $(S,R,V[p\mapsto Z])$.

We assume familiarity with the notion of bisimilarity between two (pointed) Kripke models, and say that a formula of $\mathtt{MSO}$ is bisimulation invariant if it has the same truth value in any pair of bisimilar pointed Kripke models.

Fact 8** (Janin-Walukiewicz Theorem [13]).**

A formula $\varphi$ of $\mathtt{MSO}$ is equivalent to a formula of $\mathtt{\mu ML}$ iff $\varphi$ is invariant for bisimulations.

Generally, given two languages $\mathtt{L}$ and $\mathtt{L}^{\prime}$ we shall write $\mathtt{L}\equiv\mathtt{L}^{\prime}$ to say that every formula of $\mathtt{L}$ is semantically equivalent to a formula of $\mathtt{L}^{\prime}$, and vice versa. We will denote the bisimulation invariant fragment of $\mathtt{L}$ by $\mathtt{L}/{\sim}$. With this notation we can state the previous fact more succinctly as:

[TABLE]

The proof of the Janin-Walukiewicz theorem proceeds by comparing suitable automaton models for $\mathtt{MSO}$ and the modal $\mu$-calculus. To get an understanding of how $\mathtt{MSO}$-automata on Kripke models work, the main conceptual step one needs to take from the perspective of word and stream automata is to take a logical view on the transition structure of an automaton, i.e. the transition map of an automaton will be constructed from formulas in a logical system. Let $A$ be a set (of variables). The language of first-order logic with equality over $A$ is given by the grammar:

[TABLE]

where $a\in A$ and $x,y$ belong to some fixed, countably infinite set of individual variables. The set of sentences in this language is denoted $\mathtt{FOE}(A)$, and the set of sentences in which each $a\in A$ appears positively is denoted by $\mathtt{FOE}^{+}(A)$. The fragment of $\mathtt{FOE}(A)$ in which the equality symbol does not occur is denoted by $\mathtt{FO}(A)$, and we write $\mathtt{FO}^{+}(A)$ for $\mathtt{FOE}^{+}(A)\cap\mathtt{FO}(A)$.

A model for this language, in the usual sense, is simply a set $X$ together with an assignment of a subset of $X$ to each $a\in A$, viewed as a predicate - in other words, a valuation $V:A\to\mathcal{P}(X)$. {defi} Let $P$ be a set of propositional variables. A $P$-chromatic $\mathtt{MSO}$-automaton $\mathbb{A}$ is a tuple $(A,\Delta,a_{I},\Omega)$, where $A$ is a finite set, $a_{I}\in A$, $\Omega:A\to\omega$ is a priority map and

[TABLE]

is the transition map, assigning a sentence in $\mathtt{FOE}^{+}(A)$ to each pair $(a,Q)$ with $a\in A$ and $Q\subseteq P$.

Note that, in this automaton model, the powerset of $P$ takes on the role of an alphabet of the automaton. In order to decide whether or not an automaton $\mathbb{A}$ accepts or rejects a given pointed Kripke model $\mathbb{S},s$, we define a parity game called the acceptance game for $\mathbb{A}$ with respect to the model $\mathbb{S}$. The role of $\exists$ is to act as a “defense attorney”, in favor of acceptance of the model, and the goal of $\forall$ is to act as a “prosecutor” trying to show that the model should be rejected. A “round” of this game will have the following shape: first, the automaton is in a state $a$ and is visiting some point $s$ in the model $\mathbb{S}$. At such a basic position of the acceptance game, it will be $\exists$’s turn to move, and her moves are constrained by the transition map. Formally, she needs to come up with a valuation $U:A\to\mathcal{P}(R[s])$ over the immediate successors of $s$ with respect to the accessibility relation, such that the one-step Kripke model $(R[s],U)$ satisfies the $\mathtt{FOE}^{+}(A)$-sentence $\Delta(a,V^{\dagger}(s)\cap P)$. Here, we think of $V^{\dagger}(s)\cap P$ - the collection of propositional variables in $P$ true at the point $s$ - as the input from the alphabet currently being read by the automaton. In practice, we will assume that we are dealing with a model in which the valuation $V$ assigns an empty value to each variable not in $P$, so that we may just write $V^{\dagger}(s)$ rather than $V^{\dagger}(s)\cap P$.

For a more precise description of the game, we provide the positions, player assignments, admissible moves and priorities of the acceptance game in a table:

Given $s\in S$, we say that $\mathbb{A}$ accepts the pointed model $(\mathbb{S},s)$ if $(a,s)$ is a winning position for $\exists$ in the acceptance game. In practice, we will often identify a partial match of the form:

[TABLE]

of the acceptance game belonging with the sequence of basic positions

[TABLE]

appearing in the match.

It may be helpful at this point to compare the acceptance game for these automata to the notion of acceptance we presented for stream automata in Section 2.1. In particular, the reader can may check that an accepting run of a non-deterministic parity stream automaton can be viewed as a winning strategy for $\exists$ in a parity game, but one in which the role of the opposing player $\forall$ becomes trivialized: all choices in this game will belong to $\exists$.

$\mathtt{MSO}$-formulas are not equivalent to $\mathtt{MSO}$-automata in general. To obtain the desired connection between formulas of $\mathtt{MSO}$ and $\mathtt{MSO}$-automata, it is necessary to restrict attention to pointed Kripke models $(S,R,V,u)$ that are tree-like, i.e. such that the underlying frame $(S,R)$ is a tree rooted at $u$. The following result is proved in [36]:

Fact 9**.**

For every formula $\varphi$ of $\mathtt{MSO}$ with free second-order variables $P$, there exists a $P$-chromatic $\mathtt{MSO}$-automaton accepting all and only those tree-like pointed Kripke models that satisfy $\varphi$.

A converse of this result also holds, so that any $\mathtt{MSO}$-automaton can be translated to a sentence of $\mathtt{MSO}$ that is equivalent to it over tree-like models. Furthermore, a key insight behind the Janin-Walukiewicz theorem is that $\mathtt{MSO}$ automata are very closely related to an automaton model that is suitable to model $\mu$-calculus formulas, on arbitrary Kripke models.

Fact 10**.**

A class of pointed Kripke models is definable by a formula in $\mathtt{\mu ML}$ with free variables $P$ if, and only if, it is recognized by some $P$-chromatic $\mathtt{MSO}$-automaton such that, for all $Q\subseteq P$ and $a\in A$, we have $\Delta(a,Q)\in\mathtt{FO}^{+}(A)$.

The proof of Fact 9 involves establishing a number of closure properties of $\mathtt{MSO}$-automata, corresponding to the logical connectives. For example, negation corresponds to complementation on the automata side, where the complement of an automaton $\mathbb{A}$ accepts precisely those inputs that are rejected by $\mathbb{A}$. Similarly, the union of $\mathbb{A}$ and $\mathbb{B}$ accepts precisely those inputs accepted by either $\mathbb{A}$ or $\mathbb{B}$, and corresponds to disjunction on the logical side. The most difficult property to establish is projection, corresponding to second-order quantification. The solution lies in a simulation theorem for $\mathtt{MSO}$-automata, simplifying the formulas appearing in the range of the transition map. {defi} A formula in $\mathtt{FOE}^{+}(A)$ is said to be a disjunctive formula if it is a disjunction of formulas of the form:

[TABLE]

where $a_{1},...,a_{n},b_{1},...,b_{k}\in A$ and $\mathsf{diff}(z_{1},...,z_{m})$ is an abbreviation for the formula:

[TABLE]

A $P$-chromatic $\mathtt{MSO}$-automaton $\mathbb{A}$ is said to be non-deterministic if, for all $a\in A$ and all $Q\subseteq P$, the formula $\Delta(a,Q)$ is disjunctive.

Fact 11** (Simulation of $\mathtt{MSO}$-automata).**

For every $\mathtt{MSO}$-automaton $\mathbb{A}$, there exists a non-deterministic $\mathtt{MSO}$-automaton $\mathbb{A}^{\prime}$ that accepts the same tree-like pointed Kripke models as $\mathbb{A}$.

One of our contributions in this paper is a purely semantic account of what makes disjunctive formulas useful, that is independent of their rather specific syntax and thus suitable for our more abstract setting.

3. Coalgebras and generic modal fixpoint logics

3.1. Coalgebras and models

In the general case our basic semantic structures will consist of coalgebras together with valuations. We only consider coalgebras over the base category $\mathbf{Set}$ with sets as objects and functions as arrows. The co- and contravariant power set functors will be denoted by $\mathcal{P}:\mathbf{Set}\to\mathbf{Set}$ and $\mathcal{Q}:\mathbf{Set}\to\mathbf{Set}^{op}$, respectively. We recall the actions of these functors on morphisms: given $f:X\to Y$, we have $\mathcal{P}f(Z)=f[Z]$ for $Z\subseteq X$, and $\mathcal{Q}f(Z)=f^{-1}(Z)$ for $Z\subseteq Y$. Covariant endofunctors on $\mathbf{Set}$ will be called set functors. {conv} We will make an additional assumption on all set functors here: we require that they preserve all monics in $\mathbf{Set}$, i.e. that $\mathsf{T}f$ is an injective map whenever $f$ is. This is a very mild constraint, since it very nearly holds for all set functors already, the only possible exception being maps with empty domain [32]. So throughout this paper, “set functor” will be taken to mean: “set functor that preserves all monics”. All the functors we consider here will satisfy the constraint.

{defi}

Let $\mathsf{T}$ be a set functor. A $\mathsf{T}$-coalgebra is a pair $(S,\sigma)$ consisting of a set $S$, together with a map $\sigma:S\to\mathsf{T}S$. A $\mathsf{T}$-model is a structure $\mathbb{S}=(S,\sigma,V)$ where $(S,\sigma)$ is a $\mathsf{T}$-coalgebra and $V:\mathit{Var}\rightarrow\mathcal{P}S$. A pointed $\mathsf{T}$-model is a structure $(\mathbb{S},s)$ where $\mathbb{S}$ is a $\mathsf{T}$-model and $s\in S$.

The usual notion of a $p$-morphism between Kripke models can be generalized as follows: {defi} Let $\mathbb{S}_{1}=(S_{1},\sigma_{1},V_{1})$ and $\mathbb{S}_{2}=(S_{2},\sigma_{2},V_{2})$ be two $\mathsf{T}$-models and let $f:S_{1}\rightarrow S_{2}$ be any map. Then $f$ is said to be a $\mathsf{T}$-model morphism if:

1. (1)

for each variable $p$ and each $u\in S_{1}$, we have $u\in V_{1}(p)$ iff $f(u)\in V_{2}(p)$; 2. (2)

the map $f$ is a coalgebra morphism, i.e. we have

[TABLE]

{defi}

Two pointed $\mathsf{T}$-models $(\mathbb{S},s)$ and $(\mathbb{S}^{\prime},s^{\prime})$ are said to be behaviourally equivalent, notation: $(\mathbb{S},s)\sim(\mathbb{S}^{\prime},s^{\prime})$, if $s$ and $s^{\prime}$ can be identified by morphisms $f:\mathbb{S}\to\mathbb{T}$ and $f^{\prime}:\mathbb{S}^{\prime}\to\mathbb{T}$ such that $f(s)=f^{\prime}(s^{\prime})$ (for some $\mathsf{T}$-model $\mathbb{T}$).

It is well known that coalgebras and coalgebra morphisms for a set functor form a co-complete category, since its forgetful functor creates colimits [1]. In particular this means that coproducts of arbitrary families of $\mathsf{T}$-models exist, and they correspond to disjoint unions of models in the case of Kripke semantics. Concretely, we define disjoint unions of $\mathsf{T}$-models as follows: {defi} Let $\{\mathbb{S}_{i}\}_{i\in I}$ be a family of $\mathsf{T}$-models, where $\mathbb{S}_{i}=(S_{i},\sigma_{i},V_{i})$. Then we define the disjoint union $\coprod_{i\in I}\mathbb{S}_{i}=(S^{\prime},\sigma^{\prime},V^{\prime})$ by first setting $S^{\prime}=\coprod_{i\in I}S_{i}$ to be the disjoint union of the sets $S_{i}$. Let $f_{i}$ denote the insertion map of $S_{i}$ into $S^{\prime}$. Then we define $\sigma^{\prime}$ to be the unique map with the property that $\sigma^{\prime}\circ f_{i}=\mathsf{T}f_{i}\circ\sigma_{i}$ for all $i\in I$. For $p\in\mathit{Var}$ we define $V^{\prime}(p)=\bigcup_{i\in I}f_{i}[V_{i}(p)]$.

Fact 12**.**

For each $j\in I$, the insertion map $f_{j}:\mathbb{S}_{j}\to\coprod_{i\in I}\mathbb{S}_{i}$ is a $\mathsf{T}$-model morphism.

Kripke models are $\mathsf{T}$-models for $\mathsf{T}$ equal to the (covariant) power set functor $\mathcal{P}$, and two pointed Kripke models are behaviourally equivalent iff they are bisimilar in the usual sense. Comprehensive lists of examples of coalgebraic modal logics for various type functors and their applications can be found in several research papers by various authors, see for example [5]. We shall review some of these examples later, when we consider applications of our main characterization results. One functor that will be of particular interest in this paper is the monotone neighborhood functor $\mathcal{M}$, usually defined as the subfunctor of $\mathcal{Q}\circ\mathcal{Q}$ given by setting $\mathcal{M}X\subseteq\mathcal{Q}\mathcal{Q}X$ to be:

[TABLE]

Following the usual terminology we shall often refer to $\mathcal{M}$-models as neighborhood models. There is a standard definition of bisimilarity for neighborhood models: {defi} A neighborhood bisimulation between neighborhood models $\mathbb{S}_{1}$ and $\mathbb{S}_{2}$ is a relation $R\subseteq S_{1}\times S_{2}$ such that, if $s_{1}Rs_{2}$ then:

• •

$V_{1}^{\dagger}(s_{1})=V_{2}^{\dagger}(s_{2})$;

• •

for all $Z_{1}$ in $\sigma_{1}(s_{1})$ there is $Z_{2}$ in $\sigma_{2}(s_{2})$ such that for all $t_{2}\in Z_{2}$ there is $t_{1}\in Z_{1}$ with $t_{1}Rt_{2}$;

• •

for all $Z_{2}$ in $\sigma_{2}(s_{2})$ there is $Z_{1}$ in $\sigma_{1}(s_{1})$ such that for all $t_{1}\in Z_{1}$ there is $t_{2}\in Z_{2}$ with $t_{1}Rt_{2}$.

Neighborhood bisimilarity coincides with behavioural equivalence for $\mathcal{M}$, and in the next section we shall see how neighborhood bisimulations arise from a relation lifting for $\mathcal{M}$.

In many cases, behavioural equivalence of coalgebras can be described more concretely by bisimulations defined via certain relation liftings. For some work specificially on this topic, see the following papers by Marti and Venema: [19, 20, 21]. As an example, bisimilarity of Kripke models can be described using what is known as the “Egli-Milner lifting” for the powerset functor. This lifting assigns to a relation $R\subseteq X\times Y$ the “lifted” relation $\overline{\mathcal{P}}(R)\subseteq\mathcal{P}X\times\mathcal{P}Y$ defined by:

[TABLE]

When the functor satisfies a certain condition, preservation of weak pullbacks, the appropriate relation lifting can be defined directly in terms of the functor. In the special case of endofunctors on $\mathbf{Set}$, weak pullback preservation can be described rather concretely as the following condition [9]: consider any pair of maps $f_{1}:X_{1}\to Y$ and $f_{2}:X_{2}\to Y$, and any $\alpha_{1}\in\mathsf{T}X_{1}$, $\alpha_{2}\in\mathsf{T}X_{2}$ with $\mathsf{T}f_{1}(\alpha_{1})=\mathsf{T}f_{2}(\alpha_{2})$. Let

[TABLE]

That is, $R$ together with its projection maps $\pi_{1}:R\to X_{1}$ and $\pi_{2}:R\to X_{2}$ is the pullback of the co-span $f_{1},f_{2}$ in $\mathbf{Set}$. Then $\mathsf{T}$ preserves weak pullbacks if, in this situation, we can always find some $\gamma\in\mathsf{T}R$ with $\mathsf{T}\pi_{1}(\gamma)=\alpha_{1}$ and $\mathsf{T}\pi_{2}(\gamma)=\alpha_{2}$.

Provided that $\mathsf{T}$ preserves weak pullbacks, we can define a relation lifting $\overline{\mathsf{T}}$ known as the Barr extension of $\mathsf{T}$ [3]. This is a functor on the category $\mathbf{Rel}$ of sets with binary relations as arrows, and formally its action on a relation $R\subseteq X_{1}\times X_{2}$ is defined by setting:

[TABLE]

The Egli-Milner lifting is the Barr extension of the covariant powerset functor, and bisimulations that are sound and complete for behavioural equivalence can be defined from the Barr extension of a functor in precisely the same manner as standard bisimulations are defined from the Egli-Milner lifting. This will not play a big role in the present paper, but the Barr extension will make a minor appearance when we discuss some basic facts about predicate liftings. We remark that the monotone neighborhood functor is known not to preserve weak pullbacks, so neighborhood bisimulations can not be recovered via the Barr extension. This was in fact part of the motivation behind the work on relation liftings by Marti and Venema.

3.2. The coalgebraic $\mu$-calculus

The modal $\mu$-calculus is just one in a family of logical systems that may collectively be referred to as the coalgebraic $\mu$-calculus [4]. Generally, the key notion that connects coalgebra with logic is that of a predicate lifting. Here, we recall that $\mathcal{Q}$ denotes the contravariant powerset functor, as defined in Section 3.1. {defi}

Given a set functor $\mathsf{T}$, an $n$-place predicate lifting for $\mathsf{T}$ is a natural transformation

[TABLE]

where $\mathcal{Q}^{n}$ denotes the $n$-fold product of $\mathcal{Q}$ with itself. A predicate lifting $\lambda$ is said to be monotone if

[TABLE]

whenever $Y_{i}\subseteq Z_{i}$ for each $i$. The Boolean dual $\lambda^{d}$ of $\lambda$ is defined by

[TABLE]

We shall often think of an arbitrary finite set $A$ of size $n$ as being identified with the set $\{1,...,n\}$ via some fixed one-to-one correspondence, so that we may view any natural transformation $\lambda:\mathcal{Q}^{A}\to\mathcal{Q}\circ\mathsf{T}$ as an $n$-place predicate lifting. In these cases we sometimes speak of “predicate liftings over $A$” rather than “$n$-place predicate liftings”, but note that this is merely a notational variation rather than a substantial generalization of the notion of predicate liftings. A predicate lifting $\lambda$ over $A$ can be represented equivalently as a subset of $\mathsf{T}\mathcal{P}A$, via an application of the Yoneda lemma (this observation is due to Schröder, [31]). Roughly speaking, predicate liftings are used to express “local” properties about the next unfolding of the transition map of a coalgebra, viewed from a given state of the coalgebra and using properties of states in the coalgebra as parameters.

Given a set functor $\mathsf{T}$ and a set of monotone predicate liftings $\Lambda$ for $\mathsf{T}$, the language $\mu\mathtt{ML}_{\Lambda}$ of the coalgebraic $\mu$-calculus based on $\Lambda$ is defined as follows. Again we present the language in negation normal form; note that we make sure that the modal operators of the language are closed under Boolean duals.

[TABLE]

where $p\in\mathit{Var}$, $\lambda\in\Lambda$, $\eta\in\{\mu,\nu\}$, and, in $\eta p.\varphi$, no free occurrence of the variable $p$ in $\varphi$ is in the scope of a negation. If $\Lambda$ consists of all monotone predicate liftings for $\mathsf{T}$, then we denote the language $\mu\mathtt{ML}_{\Lambda}$ also by $\mu\mathtt{ML}_{\mathsf{T}}$.

The semantics of formulas in a pointed $\mathsf{T}$-model $(\mathbb{S},s)$, where $\mathbb{S}=(S,\sigma,V)$, is defined as follows:

• •

$(\mathbb{S},s)\Vdash p$ iff $s\in V(p)$ and $(\mathbb{S},s)\Vdash\neg p$ iff $s\notin V(p)$.

• •

If $\lambda\in\Lambda$ or is the dual of some lifting in $\Lambda$, we set $(\mathbb{S},s)\Vdash\lambda(\varphi_{1},...,\varphi_{n})$ iff $\sigma(s)\in\lambda_{S}(\|\varphi_{1}\|,...,\|\varphi_{n}\|)$, where $\|\varphi_{i}\|=\{t\in S\mid(\mathbb{S},t)\Vdash\varphi_{i}\}$.

• •

Standard clauses for the boolean connectives

• •

$(\mathbb{S},s)\Vdash\mu p.\varphi$ iff $s\in\bigcap\{X\subseteq S\mid\varphi_{p}(X)\subseteq X\}$, where $\varphi_{p}(Z)$ denotes the truth set of the formula $\varphi$ in the $\mathsf{T}$-model $(S,\sigma,V[p\mapsto Z])$.

It is routine to prove that all formulas in $\mathtt{\mu ML}_{\mathsf{T}}$ are bisimulation invariant, i.e. they have the same truth value in every pair of behaviourally equivalent pointed $\mathsf{T}$-models. (We shall continue to use the term “bisimulation invariant” rather than “invariant for behavioural equivalence”, although strictly speaking bisimulation and behavioural equivalence are distinct concepts.)

{exa}

The powerset functor $\mathcal{P}$ has a unary predicate lifting $\Diamond$ defined by setting, for $\alpha\in\mathcal{P}X$:

[TABLE]

The language $\mu\mathtt{ML}_{\{\Diamond\}}$ is precisely the standard modal $\mu$-calculus $\mu\mathtt{ML}$. The dual of $\Diamond$ is denoted $\Box$, as usual. We recall its standard definition in modal logic as $\Box\psi:=\neg\Diamond\neg\psi$, which is in accordance with our definition of the dual of a predicate lifting.

{exa} The monotone neighborhood functor comes equipped with a unary predicate lifting, which we shall also denote by the symbol $\Box$. It is defined by setting, for $\alpha\in\mathcal{M}X$:

[TABLE]

In fact, we can embed $\mathcal{P}$ as a subfunctor of $\mathcal{M}$ by mapping $\alpha\in\mathcal{P}X$ to the neighborhood structure $\{Z\subseteq X\mid\alpha\subseteq Z\}$. Clearly the two predicate liftings denoted by $\Box$ both agree on this subfunctor, so it makes sense to use the same symbol to denote both. This lifting for $\mathcal{M}$ corresponds to the usual box modality for monotone modal logic, and so the language $\mu\mathtt{ML}_{\{\Box\}}$ corresponds to a fixpoint extension of monotone modal logic that we will here refer to as the monotone $\mu$-calculus, denoted $\mu\mathtt{MML}$. The logic $\mu\mathtt{MML}$ is a very natural system to study: in a sense, it is the minimal modal $\mu$-calculus since the only constraint we put on the box modality is monotonicity, which is precisely what is needed for the semantics of the fixpoint operators to be well defined. It is a well-behaved system: it was recently shown to have uniform interpolation [22], and we shall show here that it enjoys a Janin-Walukiewicz style characterization theorem.

3.3. Coalgebraic automata

Turning to the parity automata corresponding to the language $\mathtt{\mu ML}_{\Lambda}$, we first define the modal one-step language $\mathtt{1ML}_{\Lambda}$. {defi}

The set $\mathtt{1ML}_{\Lambda}(A)$ of modal one-step formulas over a set $A$ of variables is given by the following grammar:

[TABLE]

where $\psi_{1},...,\psi_{n}$ are formulas built up from variables in $A$ using disjunctions and conjunctions. More formally, we require that $\psi_{1},...,\psi_{n}\in\mathtt{Latt}(A)$ where $\mathtt{Latt}(A)$ denotes the set of lattice formulas over $A$ given by the grammar:

[TABLE]

where $a$ ranges over $A$.

{defi} Given a functor $\mathsf{T}$ and a set of variables $A$, a one-step model over $A$ is a triple $(X,\alpha,V)$ where $X$ is any set, $\alpha\in\mathsf{T}X$ and $V:A\rightarrow\mathcal{Q}(X)$ is a valuation.

Note that we have written the valuation $V$ as having the type $A\to\mathcal{Q}(X)$ rather than $A\to\mathcal{P}(X)$ in this definition. This notation is equally correct since the covariant and contravariant powerset functors differ only in their action on morphisms, and it is sometimes a more convenient notation since the naturality condition of predicate liftings is formulated in terms of $\mathcal{Q}$ and not $\mathcal{P}$.

The semantics of formulas in the modal one-step language in a one-step model is given as follows:

• •

standard clauses for the boolean connectives,

• •

$(X,\alpha,V)\Vdash_{1}\lambda(\psi_{1},...,\psi_{n})$ iff $\alpha\in\lambda_{X}(\|\psi_{1}\|_{V},...,\|\psi_{n}\|_{V})$

where $\|\psi_{i}\|_{V}\subseteq X$ is the (classical) truth set of the formula $\psi_{i}$ under the valuation $V$. Formally, this is defined by $\|\bot\|_{V}=\emptyset$, $\|\top\|_{V}=X$, $\|a\|_{V}=V(a)$ for $a\in A$, $\|\varphi\wedge\psi\|_{V}=\|\varphi\|_{V}\cap\|\psi\|_{V}$ and $\|\varphi\vee\psi\|_{V}=\|\varphi\|_{V}\cup\|\psi\|_{V}$. For $u\in X$ and a lattice formula $\psi$ we also write $u\Vdash^{0}_{V}\psi$ to say that $u\in\|\psi\|_{V}$.

Recalling that any predicate lifting over a set of $n$ variables $A$ corresponds to an $n$-place predicate lifting, we can view any predicate lifting $\lambda$ over $A$ as a one-step formula in $\mathtt{1ML}_{\{\lambda\}}(A)$333Or rather, if we want to be completely precise, $\lambda$ corresponds to a one-step formula in $\mathtt{1ML}_{\{\lambda^{\prime}\}}(A)$ where the lifting $\lambda^{\prime}:\mathcal{Q}^{n}\to\mathcal{Q}\circ\mathsf{T}$ is obtained by composing $\lambda$ with the natural isomorphism between functors $\mathcal{Q}^{n}$ and $\mathcal{Q}^{A}$ induced by some fixed bijection $i:n\to A$. If we write $A=\{a_{1},...,a_{n}\}$ with $a_{k}=f(k-1)$, this means that we have $\lambda_{X}(V)=\lambda^{\prime}_{X}(V(a_{1}),...,V(a_{n}))$. We shall permit some abuse of notation and simply identify $\lambda$ with the associated lifting $\lambda^{\prime}$. . With this mind we can write $(X,\alpha,V)\Vdash_{1}\lambda$ instead of $\alpha\in\lambda_{X}(V)$. In this notation the naturality constraint for a predicate lifting $\lambda$ over $A$ becomes, for every $\alpha\in X$, every map $f:X\to Y$ and every $V:A\to\mathcal{Q}(Y)$:

[TABLE]

We can now define the class of automata used to characterize the coalgebraic $\mu$-calculus.

{defi}

Let $P$ be a finite set of variables and $\Lambda$ a set of predicate liftings. Then a ($P$-chromatic) modal $\Lambda$-automaton is a tuple $(A,\Delta,\Omega,a_{I})$ where $A$ is a finite set of states with $a_{I}\in A$,

[TABLE]

is the transition map of the automaton, and $\Omega:A\rightarrow\omega$ is the parity map. The class of these automata is denoted as $\mathit{Aut}(\mathtt{1ML}_{\Lambda})$.

Note that there are two distinct sets of “variables” involved in the automaton $\mathbb{A}$, and it is important to keep these apart since they have different roles: the variables $P$ are used to provide the alphabet of the automaton (and correspond to free variables of corresponding fixpoint formulas), while the variables $A$ are the states of the automaton (and correspond to bound variables of a corresponding fixpoint formula.)

The acceptance game for an automaton $\mathbb{A}=(A,\Delta,\Omega,a_{I})$ and a $\mathsf{T}$-model $(S,\sigma,V)$ is the parity game given by the following table:

The loser of a finite match is the player who got stuck, and the winner of an infinite match is $\exists$ if the greatest parity that appears infinitely often in the match is even, and the winner is $\forall$ if this parity is odd. Note that the valuations $U$ and $V$ in Table 2 play fundamentally different roles: $V$ is a fixed valuation given by the model on which the automaton is run, assigning values to the open variables of the automaton, while $U$ is a “local” valuation assigning values to the states of the automaton, which correspond roughly to bound variables of a fixpoint formula.

Given a strategy $\chi$ for either player, a match is said to be $\chi$-guided if it is consistent with every choice made by that player according to $\chi$. Winning strategies are defined as usual. {defi} The automaton $\mathbb{A}$ accepts the pointed model $(\mathbb{S},s)$, written $(\mathbb{S},s)\Vdash\mathbb{A}$, if $\exists$ has a winning strategy in the acceptance game from the starting position $(a_{I},s)$. We say that an automaton $\mathbb{A}$ is equivalent to a formula $\varphi\in\mathtt{\mu ML}_{\Lambda}$ if, for every pointed $\mathsf{T}$-model $(\mathbb{S},s)$, we have that $\mathbb{A}$ accepts $(\mathbb{S},s)$ iff $(\mathbb{S},s)\Vdash\varphi$.

Fact 13**.**

[8*]**

Let $\mathsf{T}$ be a set functor, and $\Lambda$ a set of monotone predicate liftings for $\mathsf{T}$. Then*

[TABLE]

That is, there are effective transformations of formulas in $\mathtt{\mu ML}_{\Lambda}$ into equivalent automata in $\mathit{Aut}(\mathtt{1ML}_{\Lambda})$, and vice versa.

3.4. One-step expressive completeness

Our main result in this paper is formulated in terms of the set of all monotone predicate liftings for a given functor, and we would argue that this is a rather natural choice. However, in some cases it is possible to choose some smaller set of liftings, in order to have a more concrete and manageable presentation of the syntax of the corresponding $\mu$-calculus. It will then be important to choose an expressively complete set of predicate liftings, meaning that any monotone lifting for the functor can be defined by a formula in the modal one-step language. In particular, this will be required to recover the Janin-Walukiewicz theorem in its original form as a special case of our main results.

{defi}

Let $\Lambda$ be a set of monotone predicate liftings and $\lambda$ any predicate lifting over the finite set $A$. We say that $\lambda$ is $\Lambda$-definable if there is a formula $\varphi\in\mathtt{1ML}_{\Lambda}(A)$ such that, for any one-step model $(X,\alpha,V)$ we have:

[TABLE]

We say that a set of monotone predicate liftings $\Lambda$ is expressively complete if every monotone predicate lifting over any given finite set $A$ is $\Lambda$-definable.

Our main observation in this section is that any weak pullback preserving functor that also preserves finite sets has a natural choice of expressively complete predicate liftings. {defi} Given a functor $\mathsf{T}$ that preserves weak pullbacks, the $n$-ary Moss lifting corresponding to $\alpha\in\mathsf{T}\{1,...,n\}$ is the predicate lifting $\langle\alpha\rangle:\mathcal{Q}^{n}\to\mathcal{Q}\circ\mathsf{T}$ such that for all sets $X$ and $Z_{1},...,Z_{n}\subseteq X$, we have:

[TABLE]

where $R\subseteq X\times\{1,...,n\}$ is defined by $uRk$ iff $u\in Z_{k}$.

In particular, for any given lattice formulas $\psi_{1},...,\psi_{n}\in A$, any $\beta\in\mathsf{T}\{1,...,n\}$ and any one-step model $(X,\alpha,V)$ over $A$, we have:

[TABLE]

where $f:\{1,...,n\}\to\{\psi_{1},...,\psi_{n}\}$ is the map defined by $k\mapsto\psi_{k}$.

Note that the Moss lifting $\langle\alpha\rangle$ is always a natural transformation, as required: it is obtained by composing the natural transformation $h^{\alpha}:\mathcal{Q}^{n}\to\mathsf{T}\circ\mathcal{Q}$ defined by

[TABLE]

with the distributive law $\delta:\mathsf{T}\circ\mathcal{Q}\to\mathcal{Q}\circ\mathsf{T}$ defined for $\beta\in\mathsf{T}\mathcal{Q}X$ by:

[TABLE]

where $\in_{X}$ is the membership relation from $X$ to $\mathcal{Q}X$. That this distributive law is a natural transformation is a standard fact, see for example [16] where this view of Moss formulas as special predicate liftings is investigated thoroughly.

Proposition 14**.**

If $\mathsf{T}$ preserves weak pullbacks and finite sets, then the set of all Moss liftings for $\mathsf{T}$ (of all arities $n\in\omega$) is expressively complete.

Proof 3.1**.**

Fix a monotone predicate lifting $\lambda$ over $A$. Let $(X,\alpha,V)$ be any one-step model over $A$. Let $n$ be the number of lattice formulas over $A$, and let $f:\mathtt{Latt}(A)\to\{1,...,n\}$ be some fixed bijective enumeration of $\mathtt{Latt}(A)$, so that we can write

[TABLE]

Let $\theta:X\to\mathtt{Latt}(A)$ be the map sending each $u\in X$ to $\bigwedge\{a\in A\mid u\in V(a)\}$. The characteristic formula of $(X,\alpha,V)$, denoted $\chi(X,\alpha,V)$, is defined as:

[TABLE]

It is an exercise in coalgebra to show that, for any one-step model $(X^{\prime},\alpha^{\prime},V^{\prime})$, we have

[TABLE]

where we write $u\preceq u^{\prime}$, for $u\in X$ and $u^{\prime}\in X^{\prime}$, if $u\in V(a)$ implies $u^{\prime}\in V^{\prime}(a)$ for all $a\in A$. Furthemore, there are only finitely many characteristic formulas relative to any given set of variables $A$, since $\mathsf{T}$ preserves finite sets (and hence $\mathsf{T}\{1,...,n\}$ is finite). We claim that the formula:

[TABLE]

defines the monotone lifting $\lambda$. One direction is clear: if $\alpha\in\lambda_{X}(V)$ then $X,\alpha,V\Vdash_{1}\varphi$ since $(X,\alpha,V)\Vdash_{1}\chi(X,\alpha,V)$. Conversely, suppose that $X,\alpha,V\Vdash_{1}\varphi$. Then there exists some one-step model $(X^{\prime},\alpha^{\prime},V^{\prime})$ such that $\alpha^{\prime}\in\lambda_{X^{\prime}}(V^{\prime})$ and $(\alpha^{\prime},\alpha)\in\overline{\mathsf{T}}(\preceq)$. Write $R=\{(u,v)\mid u\preceq v\}$, let $\pi^{\prime}:R\to X^{\prime}$ and $\pi:R\to X$ be the projection maps, and let $\gamma\in\mathsf{T}R$ be such that $\mathsf{T}\pi^{\prime}(\gamma)=\alpha^{\prime}$ and $\mathsf{T}\pi(\gamma)=\alpha$. By naturality we get $\gamma\in\lambda_{R}(\mathcal{Q}\pi^{\prime}\circ V^{\prime})$, by monotonicity we get $\gamma\in\lambda_{R}(\mathcal{Q}\pi\circ V)$ (since $\pi^{\prime}(r)\in V^{\prime}(a)$ implies $\pi(r)\in V(a)$ for all $a\in A$), and finally by naturality again we get $\gamma\in\lambda_{X}(V)$ as required.

In the special case of the powerset functor, given a set of formulas $\{\psi_{1},...,\psi_{n}\}$ (viewed as a member of $\mathcal{P}(\mathtt{Latt}(A))$), the corresponding substitution instance of the $n$-ary Moss lifting corresponds to the usual “cover” formula $\nabla\{\psi_{1},...,\psi_{n}\}$ which is defined in terms of $\Diamond$ and its dual by:

[TABLE]

Hence, it follows from Proposition 14 that the single lifting $\Diamond$ for $\mathcal{P}$ is expressively complete.

4. Coalgebraic $\mathtt{MSO}$

4.1. Introducing coalgebraic MSO

We now introduce coalgebraic monadic second-order logic for a set functor $\mathsf{T}$ and a set of liftings $\Lambda$, and show how $\mathtt{MSO}$ can be recovered as a special case. Given a set $\Lambda$ of monotone predicate liftings, we define the syntax of the monadic second-order logic $\mathtt{MSO}_{\Lambda}$ by the following grammar:

[TABLE]

where $\lambda$ is any $n$-place monotone predicate lifting in $\Lambda$ and $p,q,q_{1},...,q_{n}\in Var$. For $\Lambda$ equal to the set of all monotone predicate liftings for $\mathsf{T}$, we write $\mathtt{MSO}_{\Lambda}=\mathtt{MSO}_{\mathsf{T}}$.

For the semantics, let $(\mathbb{S},s)$ be a pointed $\mathsf{T}$-model. We define the satisfaction relation ${\Vdash}\subseteq S\times\mathtt{MSO}_{\mathsf{T}}$ as follows:

• •

$(\mathbb{S},s)\Vdash\mathsf{sr}(p)$ iff $V(p)=\{s\}$,

• •

$(\mathbb{S},s)\Vdash p\subseteq q$ iff $V(p)\subseteq V(q)$,

• •

$(\mathbb{S},s)\Vdash\lambda(p,q_{1},...,q_{n})$ iff $\sigma(v)\in\lambda_{S}(V(q_{1}),..,V(q_{n}))$ for all $v\in V(p)$,

• •

standard clauses for the Boolean connectives,

• •

$(\mathbb{S},s)\Vdash\exists p.\varphi$ iff $(S,\sigma,V[p\mapsto Z],s)\Vdash\varphi$, some $Z\subseteq S$.

We introduce the following abbreviations:

• •

$p=q$ for $p\subseteq q\wedge q\subseteq p$,

• •

$\mathsf{Em}(p)$ for $\forall q.(p\subseteq q)$,

• •

$\mathsf{Sing}(p)$ for $\neg\mathsf{Em}(p)\wedge\forall q(q\subseteq p\rightarrow(\mathsf{Em}(q)\vee q=p)),$

expressing, respectively, that $p$ and $q$ are equal, that $p$ denotes the empty set, and that $p$ denotes a singleton.

Clearly, standard $\mathtt{MSO}$ is a notational variant of the logic $\mathtt{MSO}_{\{\Diamond\}}$, since the formula $R(p,q)$ has precisely the same satisfaction clause as $\Diamond(p,q)$ - to see this, one just has to unfold the definitions. We can state the Janin-Walukiewicz theorem in a formula as:

[TABLE]

The following useful fact is fairly easy to check, so we leave its proof to the reader:

Fact 15**.**

If $\Lambda$ is a one-step expressively complete set of predicate liftings, then $\mathtt{MSO}_{\Lambda}\equiv\mathtt{MSO}_{\mathsf{T}}$ and $\mu\mathtt{ML}_{\Lambda}\equiv\mu\mathtt{ML}_{\mathsf{T}}$.

Since we know that $\Diamond$ is expressively complete we can now state the Janin-Walukiewicz theorem in yet another form, where we recall that $\mathcal{P}$ is the covariant powerset functor:

[TABLE]

Generally, we let $\mathtt{MSO}_{\mathsf{T}}/{\sim}$ denote the fragment of $\mathtt{MSO}_{\mathsf{T}}$ that is invariant for behavioural equivalence, and we refer to it as the *bisimulation invariant fragment * of $\mathtt{MSO}_{\mathsf{T}}$.

As mentioned in the introduction, the key question in this paper will be to compare the expressive power of coalgebraic monadic second-order logic to that of the coalgebraic $\mu$-calculus. The following observation, of which the (routine) proof is omitted, provides the easy part of the link.

Proposition 16**.**

Let $\Lambda$ be a set of monotone predicate liftings for the set functor $\mathsf{T}$. There is an inductively defined translation $(\cdot)^{\diamond}$ mapping any formula $\varphi\in\mathtt{\mu ML}_{\Lambda}$ to a semantically equivalent formula $\varphi^{\diamond}\in\mathtt{MSO}_{\Lambda}$.

Considering the lifting $\Box$ for $\mathcal{M}$, we introduce the name monotone monadic second-order logic for the language $\mathtt{MSO}_{\{\Box\}}$, which we will henceforth denote by $\mathtt{MMSO}$. Note that the atomic formula $\Box(p,q)$ encodes a pattern of quantifier alternation of the form $\forall\exists\forall$: it says that every state that satisfies $p$ has some neighborhood $Z$ such that every state in $Z$ satisfies $q$.

4.2. Automata for coalgebraic $\mathtt{MSO}$

In this section we introduce automata for coalgebraic monadic second-order logic, and translate formulas of $\mathtt{MSO}_{\Lambda}$ into automata operating on tree-like coalgebras.

Since the translation of standard $\mathtt{MSO}$ into parity automata is valid only over trees and not over Kripke frames in general, we should expect that coalgebraic monadic second-order logic similarly translates into parity automata over a restricted class of $\mathsf{T}$-models that are in some sense “tree-like”. So we need to start by spelling out exactly what this means.

{defi}

Given a set $S$ and $\alpha\in\mathsf{T}S$, a subset $X\subseteq S$ is said to be a support for $\alpha$ if there is some $\beta\in\mathsf{T}X$ with $\mathsf{T}\iota_{X,S}(\beta)=\alpha$. A supporting Kripke frame for a $\mathsf{T}$-coalgebra $(S,\sigma)$ is a binary relation $R\subseteq S\times S$ such that, for all $u\in S$, $R(u)=\{v\mid uRv\}$ is a support for $\sigma(u)$.

Given that $X\subseteq S$ is a support for $\alpha\in\mathsf{T}S$, our convention that $\mathsf{T}$ preserves all injectives guarantees that there is a unique $\alpha^{\prime}\in\mathsf{T}X$ such that $\mathsf{T}\iota_{X,S}(\alpha^{\prime})=\alpha$. We shall denote this $\alpha^{\prime}$ by $\alpha|_{X}$. Intuitively, $X$ is a support for $\alpha$ if we can know all there is to know about $\alpha$ just by looking at its restriction $\alpha|_{X}$ to $X$.

{defi}

A $\mathsf{T}$-tree model is a structure $(\mathbb{S},R,u)$ where $\mathbb{S}=(S,\sigma,V)$ is a $\mathsf{T}$-model and $u\in S$, such that $R$ is a supporting Kripke frame for the coalgebra $(S,\sigma)$, and furthermore $(S,R)$ is a tree rooted at $u$ (i.e. there is a unique $R$-path from $u$ to $w$ for each $w\in S$).

Our goal is to translate formulas in $\mathtt{MSO}_{\mathsf{T}}$ to equivalent automata over $\mathsf{T}$-tree models. We start by introducing a very general type of automaton, originating with [35]. The motivation for taking this general perspective is to emphasize that many automata theoretic concepts and basic results apply already in this setting, and we believe the general automaton concept we introduce here has some independent theoretical interest.

{defi}

Given a finite set $A$, a generalized predicate lifting over $A$ comprises an assignment of a map

[TABLE]

to every set $X$. Concepts like boolean dual and monotonicity apply to these liftings in the obvious way.

The difference with respect to standard predicate liftings is that the components of a generalized predicate lifting do not need to form a natural transformation. Throughout the rest of the paper, the term “predicate lifting” will be reserved for the subclass of general predicate liftings that satisfy the naturality constraint, i.e. predicate liftings in the usual sense. 444 In the style of abstract logic, it would make sense to require a generalized predicate lifting to be natural with respect to certain maps, the natural choice in this case being bijections. For the purpose of this paper such a restriction is not needed, however.

{defi}

A one-step language $\mathtt{L}$ for a functor $\mathsf{T}$ consists of a collection $\mathtt{L}(A)$ of generalized predicate liftings for $\mathsf{T}$, for every finite set $A$.

As for ordinary predicate liftings, given a generalized predicate lifting $\varphi$ and a one-step model $(X,\alpha,V)$ we sometimes write $(X,\alpha,V)\Vdash_{1}\varphi$ rather than $\alpha\in\varphi_{X}(V)$.

Our automata will be indexed by a (finite) set of variables involved, corresponding to the set of free variables of the $\mathtt{MSO}_{\mathsf{T}}$-formula.

{defi}

Let $P\subseteq\mathit{Var}$ be a finite set of variables and let $\mathtt{L}$ be a one-step language for the functor $\mathsf{T}$. A ($P$-chromatic) $\mathtt{L}$-automaton is a structure $(A,\Delta,\Omega,a_{I})$ where

• •

$A$ is a finite set, with $a_{I}\in A$,

• •

$\Omega:A\rightarrow\omega$ is a parity map, and

• •

$\Delta:A\times\mathcal{P}(P)\rightarrow\mathtt{L}(A)$ is the transition map of $\mathbb{A}$.

There are two main differences between these automata and the modal automata we have considered in Section 3.3; first, we have dropped the naturality constraint on the one-step language. Second, these automata will run on $\mathsf{T}$-tree models rather than $\mathsf{T}$-models. The acceptance game of $\mathbb{A}$ with respect to a $\mathsf{T}$-tree model $(T,R,\sigma,V,u)$ is given by Table 3. We say that the automaton $\mathbb{A}$ accepts the model $(T,R,\sigma,V,u)$ if $\exists$ has a winning strategy in this game (initialized at position $(a_{I},u)$).

4.3. Closure properties

The abstract perspective of generalized predicate liftings is useful for establishing some simple closure properties of automata, based on properties of the one-step language. The first, easy, results establish sufficient conditions for closure under union and complementation.

Proposition 17**.**

If the one-step language $\mathtt{L}$ is closed under disjunction, then the class of $\mathtt{L}$-automata is closed under union.

{defi}

An $\mathtt{L}$-automaton $\mathbb{A}$ is said to be monotone if, for all $a\in A$ and all colors $c\in\mathcal{P}(P)$, the generalized lifting $\Delta(a,c)$ is monotone in each variable in $A$.

Proposition 18**.**

If the monotone fragment of the one-step language $\mathtt{L}$ is closed under boolean duals, then the class of monotone $\mathtt{L}$-automata is closed under complementation.

The most interesting property concerns closure under existential projection. {defi} Let $\mathbb{A}$ be a $P$-chromatic $\mathtt{L}$-automaton, and let $p\in P$. Then a $P\setminus\{p\}$-chromatic $\mathtt{L}$-automaton $\mathbb{B}$ is said to be an existential projection of $\mathbb{A}$ if it accepts a $\mathsf{T}$-tree model $(T,R,\sigma,V,u)$ precisely when there is some $Z\subseteq T$ such that $\mathbb{A}$ accepts $(T,R,\sigma,V[p\mapsto Z],u)$.

The following notion originates with [13], but instead of relying on a particular syntactic shape of one-step formulas as in  [13], we define the concepts in purely semantic terms.

{defi}

A generalized predicate lifting $\varphi$ over $A$ is said to be disjunctive if, for every one-step model $(X,\alpha,V)$ such that

[TABLE]

there is a valuation $V^{*}:A\rightarrow\mathcal{Q}(X)$ such that

• •

$V^{\ast}(a)\subseteq V(a)$ for each $a\in A$,

• •

$V^{\ast}(a)\cap V^{\ast}(b)=\emptyset$ whenever $a\neq b$, and

• •

$(X,\alpha,V^{*})\Vdash_{1}\varphi$.

The second clause can also be stated as: $(V^{*})^{\dagger}(u)$ is either empty or a singleton, for all $u\in X$. Call an $\mathtt{L}$-automaton non-deterministic if every generalized lifting $\Delta(a,c)$ is disjunctive.

It is easy to see that if the language $\mathtt{L}$ is closed under disjunctions, then so is its disjunctive fragment. From this we obtain the following.

Proposition 19**.**

If the one-step language $\mathtt{L}$ is closed under disjunction, then the class of non-deterministic $\mathtt{L}$-automata is closed under existential projection over $\mathsf{T}$-tree models.

Proof 4.1**.**

Suppose $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ is a non-deterministic $\mathtt{L}$-automaton for the variable set $P$. Define the $P\setminus\{p\}$-chromatic automaton $\exists p.\mathbb{A}=(A,\Delta^{*},a_{I},\Omega)$ by setting

[TABLE]

Every $\mathsf{T}$-tree model accepted by $\mathbb{A}$ is also accepted by $\exists p.\mathbb{A}$, since any admissible move for $\exists$ at a position $(a,u)$ in the acceptance game for $\mathbb{A}$ is an admissible move at the same position in the acceptance game for $\exists p.\mathbb{A}$ too, by definition of the transition map $\Delta^{*}$.

Conversely, suppose $\exists p.\mathbb{A}$ accepts some $\mathsf{T}$-tree model $(S,R,\sigma,V,s_{I})$. For each winning position $(a,s)$ in the acceptance game, let $V_{(a,s)}$ be the valuation chosen by $\exists$ according to some given winning strategy $\chi$. Note that we can assume that $\chi$ is a positional winning strategy, since $\exists p.\mathbb{A}$ is a parity automaton. Since disjunctive formulas are closed under disjunctions, the automaton $\exists p.\mathbb{A}$ is a non-deterministic automaton, and so for each winning position $(a,s)$ there is a valuation $V_{(a,s)}^{*}:A\rightarrow\mathcal{P}(R(s))$, which is an admissible move for $\exists$, such that $V_{(a,s)}^{*}(b)\subseteq V_{(a,s)}(b)$ and such that for all $b_{1}\neq b_{2}\in A$ we have $V_{(a,s)}^{*}(b_{1})\cap V_{(a,s)}^{*}(b_{2})=\emptyset$. Define the strategy $\chi^{*}$ by letting $\exists$ choose the valuation $V_{(a,s)}^{*}$ at each winning position $(a,s)$ - this is still a winning strategy, since the valuations chosen by $\exists$ are smaller and so no new choices for $\forall$ are introduced. Furthermore, $\chi^{*}$ is clearly still a positional winning strategy.

From these facts it follows by a simple induction on the depth of the nodes in the supporting tree that the strategy $\chi^{*}$ is separating, i.e. that for every $s\in S$ there is at most one automaton state $a$ such that $(a,s)$ appears in a $\chi^{*}$-guided match of the acceptance game. So we can define a valuation $V^{\prime}$ like $V$ except we evaluate $p$ to be true at all and only the states $s$ such that

[TABLE]

where $a_{s}$ is a necessarily unique automaton state such that $(a,s)$ appears in some $\chi^{*}$-guided match, and $c$ is the color consisting of the variables true under $V$ at $s$. Then $\mathbb{A}$ accepts $(S,R,\sigma,V^{\prime},s_{I})$, by the positional strategy mapping each position $(a,s)$ to the valuation $\chi^{*}(a,s)$. That is, $\exists$ can play the same strategy $\chi^{*}(a,s)$, now viewed as a strategy in the acceptance game for $\mathbb{A}$.

4.4. Second-order automata

We now introduce a concrete one-step language for a given set functor $\mathsf{T}$ and a given set of monotone predicate liftings $\Lambda$, and show that $\mathtt{MSO}_{\Lambda}$ can be translated into the corresponding class of automata. By the closure properties established in the previous section, the language needs to be closed under disjunction and negation, and furthermore we need to establish that every automaton for this language is equivalent to a non-deterministic automaton. {defi} Let $\Lambda$ be a set of monotone predicate liftings for $\mathsf{T}$. The set of second-order one-step formulas over any set of variables $A$ and relative to the set of liftings $\Lambda$ is defined by the grammar:

[TABLE]

where $a,b,a_{1},...,a_{n}\in A$ and $\lambda$ is any predicate lifting in $\Lambda$.

The semantics of a second-order one-step formula in a one-step model $(X,\alpha,V)$ (with $V:A\to\mathcal{P}(X)$) is defined by the following clauses:

• •

$(X,\alpha,V)\Vdash_{1}a\subseteq b$ iff $V(a)\subseteq V(b)$,

• •

$(X,\alpha,V)\Vdash_{1}\lambda(a_{1},...,a_{n})$ iff $\alpha\in\lambda_{X}(V(a_{1}),...,V(a_{n}))$,

• •

standard clauses for the Boolean connectives,

• •

$(X,\alpha,V)\Vdash_{1}\exists a.\varphi$ iff $(X,\alpha,V[a\mapsto S])\Vdash_{1}\varphi$ for some $S\subseteq X$.

Fixing an infinite set of “one-step variables” $\mathsf{Var}_{1}$, and given a finite set $A$, the set of second-order one-step sentences over $A$, denoted $\mathtt{1SO}_{\Lambda}(A)$, is the set of one-step formulas over $A\cup\mathsf{Var}_{1}$, with all free variables belonging to $A$.

Remark 20**.**

The difference between the one-step language $\mathtt{1SO}_{\Lambda}(A)$ and the full language $\mathtt{MSO}_{\Lambda}$ may seem rather subtle at first sight. It is important to note that an $n$-place predicate lifting now corresponds to an $n$-place predicate in the language, not an $n+1$-place predicate as in $\mathtt{MSO}_{\Lambda}$. While the formula $\lambda(q_{1},...,q_{n})$ of $\mathtt{1SO}_{\Lambda}(A)$ expresses a proposition about the specific, fixed object $\alpha$ in a given one-step model, the formula $\lambda(p,q_{1},...,q_{n})$ in $\mathtt{MSO}_{\Lambda}$ rather describes the transition map of a coalgebra as a whole: it says that the condition $\lambda(q_{1},...,q_{n})$ holds for the unfolding of each state $s$ that satisfies $p$.

Any second-order one-step $A$-sentence $\varphi$ can be regarded as a generalized predicate lifting over $A$, with

[TABLE]

In particular, general concepts like monotonicity and closure under boolean duals apply to second-order one-step sentences. Also, note that second-order sentences are invariant under a natural notion of isomorphism:

{defi}

An isomorphism between two one-step models $(X_{1},\alpha_{1},V_{1})$ and $(X_{2},\alpha_{2},V_{2})$ is a bijection $i:X_{1}\to X_{2}$ such that $\mathsf{T}i(\alpha_{1})=\alpha_{2}$ and $V_{1}^{\dagger}(u)=V_{2}^{\dagger}(i(u))$ for each $u\in X_{1}$.

Proposition 21**.**

Given any set of predicate liftings $\Lambda$ and a set of variables $A$, any two isomorphic one-step models satisfy the same formulas in the one-step language $\mathtt{1SO}_{\Lambda}(A)$.

We can now introduce second-order automata; since every sentence in $\mathtt{1SO}_{\Lambda}(A)$ corresponds to a generalized predicate lifting, we may view $\mathtt{1SO}_{\Lambda}$ (the assignment of the one-step second-order $A$-sentences $\mathtt{1SO}_{\Lambda}(A)$ to every set of variables $A$) as a one-step language in the sense of Definition 4.2. Hence the following definition is sound:

{defi}

Let $\Lambda$ be a set of monotone predicate liftings for $\mathsf{T}$. A second-order $\Lambda$-automaton is an $\mathtt{1SO}_{\Lambda}$-automaton. We write $\mathit{Aut}(\mathtt{1SO}_{\Lambda})$ to denote this class, and $\mathit{Aut}(\mathtt{1SO}_{\mathsf{T}})$ in case $\Lambda$ is the set of all monotone predicate liftings for $\mathsf{T}$.

Formulas of $\mathtt{1SO}_{\mathsf{T}}(A)$ are not in general monotone in the variables $A$ since negation is present in the language (unlike the one-step language $\mathtt{1ML}_{\Lambda}$). However, a useful trick due to Walukiewicz allows us at any time to safely replace all one-step formulas in an automaton by monotone ones:

Proposition 22**.**

Let $\Lambda$ be any set of monotone predicate liftings. Then every second-order automaton $\mathbb{A}\in\mathit{Aut}(\mathtt{1SO}_{\Lambda})$ is equivalent to a monotone second-order automaton $\mathbb{A}\in\mathit{Aut}(\mathtt{1SO}_{\Lambda})$.

Proof 4.2**.**

Enumerate $A$ as $\{a_{1},...,a_{k}\}$, and just replace each formula $\Delta(a,c)$ by

[TABLE]

where $\Delta(a,c)[(z_{i}/a_{i})_{i\in\{1,...,k\}}]$ is the result of substituting the variable $z_{i}$ for each open variable $a_{i}$ in $\Delta(a,c)$. This new formula is monotone in the variables $A$ and the resulting automaton is equivalent to $\mathbb{A}$.

Our aim in this section is to show that every formula of $\mathtt{MSO}_{\Lambda}$ is equivalent to a monotone second-order $\Lambda$-automaton, and we shall prove this by induction on the complexity of a formula. By the previous proposition, it suffices at each step to prove the existence of a second-order $\Lambda$-automaton equivalent to the given formula, since this automaton is then guaranteed to be equivalent to a monotone one. So the induction proceeds as follows: first, we produce second-order automata equivalent to all atomic formulas. By Proposition 22 this gives us monotone second-order automata for all atomic formulas. Then, for the inductive steps, we assume that we are given monotone second-order automata equivalent to $\varphi$ and $\psi$ respectively. Our aim is to produce second-order automata that are equivalent to $\varphi\vee\psi$, $\neg\varphi$ and $\exists p.\varphi$, and once this is established we can apply Proposition 22 again to finish the induction.

For the atomic formulas, we present only the case of formulas of the form $\lambda(p,q_{1},...,q_{n})$. First, note that by naturality of $\lambda$, we have for any given $\mathsf{T}$-tree model $(\mathbb{S},R,s)$ that $(\mathbb{S},R,s)\Vdash\lambda(p,q_{1},...,q_{n})$ if, and only if, for each $u\in V(p)$:

[TABLE]

With this in mind, it is not hard to check that the following automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ is equivalent to $\lambda(p,q_{1},...,q_{n})$ over $\mathsf{T}$-tree models, where:

• •

$A=\{a_{I},b_{1},...,b_{n}\}$

• •

$\Omega(a_{I})=\Omega(b_{1})=...=\Omega(b_{n})=0$

• •

\Delta(a_{I},c)=\left\{\begin{array}[]{ll}\forall z.z\subseteq a_{I}&\text{ if }p\notin c\\ \lambda(b_{1},...,b_{n})\wedge\forall z.z\subseteq a_{I}&\text{ if }p\in c\end{array}\right\}

• •

\Delta(b_{i},c)=\left\{\begin{array}[]{ll}\bot&\text{ if }q_{i}\notin c\\ \top&\text{ if }q_{i}\in c\end{array}\right\}

Intuitively, this automaton goes on indefinitely searching the underlying tree of the model for states that satisfy $p$, and whenever it finds such a state $u$ it checks whether $u\in\lambda_{S}(V(q_{1}),...,V(q_{n}))$.

For the induction, we treat the Boolean cases first: the one-step language is clearly closed under disjunction, so second-order $\Lambda$-automata are closed under union by Proposition 17. For negation, suppose we have a monotone second-order automaton $\mathbb{A}$ equivalent to $\varphi$. It is not hard to show that for any monotone one-step formula we can define its Boolean dual in the one-step language, and furthermore the dual is again monotone. Hence, since $\mathbb{A}$ was monotone, we find an automaton $\mathbb{B}$ equivalent to $\neg\varphi$ by Proposition 18. To complete the translation of $\mathtt{MSO}_{\Lambda}$ into second-order $\Lambda$-automata we now only need to prove closure under existential projection.

4.5. A coalgebraic simulation theorem

In this section we prove that (monotone) second-order $\Lambda$-automata are closed under existential projection. The key to this result is to prove a simulation theorem, showing that every second-order automaton is equivalent to a non-deterministic one. The result then follows from Proposition 19.

The intuition behind the simulation theorem is the same as that behind the standard “powerset construction” for word automata: the states of the new non-deterministic automaton $\mathbb{A}_{n}$ are “macro-states” representing several possible states of $\mathbb{A}$ at once. Formally, the states of $\mathbb{A}_{n}$ will be binary relations over $A$, and given a macro-state $R$, its range gives an exact description of the states in $\mathbb{A}$ that are currently being visited simultaneously. It is safe to think of the macro-states as subsets of $A$, however: the only reason that we have binary relations over $A$ as states rather than just subsets is to have a memory device so that we can keep track of traces in infinite matches. For each macro-state $R$ and each colour $c$ we want to be able to say that the one-step formulas corresponding to each state in the range of $R$ hold, so we want to translate the one-step formulas over $A$ into one-step formulas over the set of macro-states. In order to translate a formula $\Delta(a,c)$ to a new one-step formula with macro-states as variables, we have to replace the variable $b$ in $\Delta(a,c)$ with a new variable that acts as a stand-in for $b$. For this purpose we introduce a new, existentally quantified variable $z_{b}$, together with a formula stating explicitly that $z_{b}$ is to represent a “disjunction” of all those macro states that contain $b$. Furthermore we want all the one-step formulas to be disjunctive, and for this purpose we simply add a conjunct “$\mathsf{Disj}$” to each one-step formula, stating that the values of any pair of distinct variables appearing in the formula are to be disjoint. Finally, in order to turn $\mathbb{A}_{n}$ into a parity automaton, we use a stream automaton to detect bad traces (see for instance [34] for the details in a more specific case).

Theorem 23** (Simulation).**

Let $\Lambda$ be a set of monotone predicate liftings for $\mathsf{T}$. For any monotone automaton $\mathbb{A}\in\mathit{Aut}({\mathtt{1SO}_{\Lambda}})$ there exists an equivalent non-deterministic $\mathbb{A}^{\prime}\in\mathit{Aut}({\mathtt{1SO}_{\Lambda}})$.

Fix an automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega)$. We consider the set $\mathcal{P}(A\times A)$ of binary relations over $A$ as a set of variables. Let

[TABLE]

This formula says that any two distinct relations, viewed as variables, are given disjoint values. Note that the formula does not express the obviously contradictory condition that any two relations $R\neq R^{\prime}\subseteq A\times A$ themselves are disjoint! Relations over $A$ are here being treated as formal variables, and the formula is true in any one-step model $(X,\alpha,V)$ such that $V(R)\cap V(R^{\prime})=\emptyset$ whenever $R\neq R^{\prime}$.

Pick a fresh variable $z_{a}$ for each $a\in A$. Given a 1-step formula $\varphi$, let

[TABLE]

be the result of substituting $z_{a}$ for each free variable $a\in A$ in $\varphi$. If we enumerate the elements of $A$ as $a_{1},...,a_{k}$, we now define the formula $\mathsf{Sim}(\varphi,b)$ for $b\in A$ to be

[TABLE]

where $\mathsf{Rep}(z_{a_{i}},\{R^{\prime}\mid(b,a_{i})\in R^{\prime}\})$ is the formula:

[TABLE]

In informal terms, the formula $\mathsf{Rep}(z_{a_{i}},\{R^{\prime}\mid(b,a_{i})\in R^{\prime}\})$ says that the variable $z_{a_{i}}$ represents a disjunction of all the macro-states that contain $a_{i}$. The formula $\mathsf{Sim}(\varphi,b)$ can thus be thought of as reformulating the formula $\varphi$ in terms of macro-states.

Let $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ be any monadic $\Lambda$-automaton. We can assume w.l.o.g. that $\mathbb{A}$ is monotone. We first construct the automaton $\mathbb{A}_{n}=(A_{n},\Delta_{n},a_{I}^{*},F)$ with a non-parity acceptance condition $F\subseteq(A_{n})^{\omega}$ as follows:

• •

$A_{n}=\mathcal{P}(A\times A)$

• •

$\Delta_{n}(R,c)=\mathsf{Disj}\wedge\bigwedge_{b\in\pi_{2}[R]}\mathsf{Sim}(\Delta(b,c),b)$

• •

$a_{I}^{\ast}=\{(a_{I},a_{I})\}$

• •

$F$ is the set of streams over $\mathcal{P}(A\times A)$ with no bad traces.

Here, $\pi_{2}$ is the second projection of a relation $R$ so that $\pi_{2}[R]$ denotes the range of $R$. A trace in a stream $(R_{1},R_{2},R_{3},...)$ over $\mathcal{P}(A\times A)$ is a stream $(a_{1},a_{2},a_{3},...)$ over $A$ with $a_{1}\in\pi_{2}[R_{1}]$ and $(a_{j-1},a_{j})\in R_{j}$ for $j>1$. A trace is bad if the greatest number $n$ with $\Omega(a_{i})=n$ for infinitely many $a_{i}$ is odd.

Proposition 24**.**

The automaton $\mathbb{A}_{n}$ is disjunctive.

Proof 4.3**.**

Since every formula $\Delta(R,c)$ contains the formula $\mathsf{Disj}$ as a conjunct, any one-step model $(X,\alpha,V)$ that satisfies $\Delta(R,c)$ must be such that $V(R)\cap V(R^{\prime})=\emptyset$ whenever $R\neq R^{\prime}$. Clearlty, this means that each formula $\Delta(R,c)$ is disjunctive.

The following lemma is routine to check, so we leave it to the reader:

Lemma 25**.**

$\mathbb{A}_{n}$* accepts precisely the same $\mathsf{T}$-tree models as $\mathbb{A}$.*

Proof 4.4** (Proof of Theorem 23).**

The only thing left to do at this point is to transform the automaton $\mathbb{A}_{n}$ into an equivalent one that has its acceptance condition given by a parity map. We make use of the following proposition (see [34]):

Claim 26**.**

The set $F$ of streams over $\mathcal{P}(A\times A)$ that contain no bad traces w.r.t. the parity map $\Omega$ is an $\omega$-regular stream language over the alphabet $\mathcal{P}(A\times A)$.

By Claim 26, there exists a deterministic parity stream automaton

[TABLE]

that recognizes the language $F$, with $\delta:Z\times\mathcal{P}(A\times A)\rightarrow Z$. We now construct the automaton

[TABLE]

as follows:

• •

$A_{n}^{\prime}=A_{n}\times Z$**

• •

$a_{I}^{\prime}=(a_{I}^{*},z_{I})$**

• •

$\Omega_{n}^{\prime}(R,z)=\Omega(z)$**

• •

$\Delta_{n}^{\prime}((R,z),c)=\Delta_{n}(R,s)[((R^{\prime},\delta(R,z))/R^{\prime})_{R^{\prime}\in\mathcal{P}(A\times A)}]$**

It is not difficult to check that $\mathbb{A}_{n}\odot\mathbb{Z}$ is equivalent to $\mathbb{A}_{n}$. Since $\mathbb{A}_{n}\odot\mathbb{Z}$ is clearly still a non-deterministic automaton, this ends the proof of the simulation theorem.

Combining Proposition 19 with Theorem 23, we obtain closure under existential projection.

Proposition 27**.**

Let $\Lambda$ be a set of monotone predicate liftings for a set functor $\mathsf{T}$. Over $\mathsf{T}$-tree models, the class of second-order $\Lambda$-automata is closed under existential projection.

We can now combine the closure properties we have established for second-order automata to give the desired translation of $\mathtt{MSO}_{\mathsf{T}}$ into second-order automata:

Theorem 28**.**

For every formula $\varphi\in\mathtt{MSO}_{\Lambda}$ with free variables in $P$, there exists a monotone $P$-chromatic second-order $\Lambda$-automaton $\mathbb{A}_{\varphi}\in\mathit{Aut}(\mathtt{1SO}_{\Lambda})$ which is equivalent to $\varphi$ over $\mathsf{T}$-tree models.

Proof 4.5**.**

It suffices to show that every formula $\varphi$ is equivalent to a $P$-chromatic $\Lambda$-automaton, since the monotonicity constraint can then be taken care of using Proposition 22. We prove the theorem by induction on the complexity of $\mathtt{MSO}_{\Lambda}$-formulas. We already showed that equivalent automata are available for the atomic formulas of $\mathtt{MSO}_{\Lambda}$. The induction step for disjunctions follows immediately from Proposition 17, since the one-step language $\mathtt{1SO}_{\Lambda}$ is clearly closed under disjunctions. The induction step for negations similarly follows from Proposition 18 once we check that the monotone fragment of the one-step language $\mathtt{1SO}_{\Lambda}$ is closed under boolean duals (here, we are again appealing to Proposition 22, to ensure that it suffices to show that monotone second-order automata are closed under complementation). To see this, suppose that $\psi\in\mathtt{1SO}_{\Lambda}(A)$ is a monotone one-step sentence, and suppose the free variables of $\psi$ are $a_{1},...,a_{n}\in A$. For each $a_{i}$, add a fresh variable $p_{i}$, and let $\mathsf{Comp}(p_{i},a_{i})$ be the formula:

[TABLE]

Informally, this formula says that $p_{i}$ is the complement of $a_{i}$. Now, let $\psi^{\partial}$ be defined as:

[TABLE]

Then $\psi^{\partial}$ is a monotone formula with free variables $a_{1},...,a_{n}$, and its semantics in a one-step model is indeed that of the boolean dual of $\psi$.

Finally, the induction step for the existential second-order quantifier is handled as follows: suppose that $\mathbb{A}$ is a $P$-chromatic second-order automaton equivalent over $\mathsf{T}$-tree models to the formula $\varphi$ and let $p\in P$. By Theorem 23, we may assume without loss of generality that $\mathbb{A}$ is disjunctive. By Proposition 19, there is a $P\setminus\{p\}$-chromatic second-order automaton $\exists p.\mathbb{A}$ that defines the projection of $\mathbb{A}$ with respect to the variable $p$. Hence, this automaton is equivalent to $\exists p.\varphi$ as required.

Corollary 29**.**

Suppose $\Lambda$ is an expressively complete set of monotone predicate liftings for $\mathsf{T}$. Then for every formula of $\mathtt{MSO}_{\mathsf{T}}$, there exists an equivalent second-order $\Lambda$-automaton over $\mathsf{T}$-tree models.

5. Bisimulation invariance

5.1. Uniform translations

This section continues the program of [35], making use of the automata-theoretic translation of $\mathtt{MSO}_{\mathsf{T}}$ we have just established. The gist of our approach is that, in order to characterize a coalgebraic fixpoint logic $\mathtt{\mu ML}_{\mathsf{T}}$ as the bisimulation-invariant fragment of $\mathtt{MSO}_{\mathsf{T}}$, it suffices to establish a certain type of translation between the corresponding one-step languages. First we need some definitions.

{defi}

Given sets $X,Y$, a mapping $h:X\rightarrow Y$ and a valuation $V:A\rightarrow\mathcal{Q}(Y)$, we define the valuation $V_{[h]}:A\rightarrow\mathcal{Q}(X)$ by setting $V_{[h]}(b)=h^{-1}(V(b))$ for each $b\in A$. In other words:

[TABLE]

Note that for a pair of composable maps $f,g$, we have $V_{[f\circ g]}=(V_{[g]})_{[f]}$. The most important concept that we take from [35] is that of a uniform translation (called uniform correspondence in [35]).

{defi}

A one-step frame is a pair $(X,\alpha)$ with $\alpha\in\mathsf{T}X$. A morphism of one-step frames $h:(X^{\prime},\alpha^{\prime})\to(X,\alpha)$ is a map $h:X^{\prime}\to X$ with $\mathsf{T}h(\alpha^{\prime})=\alpha$. A one-step frame $(X^{\prime},\alpha^{\prime})$ together with a morphism $h:(X^{\prime},\alpha^{\prime})\to(X,\alpha)$ is called a cover of $(X,\alpha)$.

We can now define the notions of uniform translations and uniform constructions: {defi} Given a functor $\mathsf{T}$, a uniform construction for $\mathsf{T}$ is an assignment of a cover $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ to every one-step frame $(X,\alpha)$.

We will usually denote the uniform construction consisting of an assignment of covers $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ simply by $(-)_{*}$.

Remark 30**.**

A good way to think of what uniform constructions will achieve, when we use them to obtain a characterization theorem later, is as methods to neutralize all the powers of distinction that the second-order one-step language has over the modal one-step language $\mathtt{1ML}_{\Lambda}$. Given two one-step models that cannot be distinguished by the modal one-step language, we want to apply suitable uniform constructions to re-shape these models so that they cannot be distinguished by the second-order one-step language either. For example, the second-order one-step language for the powerset functor is equivalent to first-order monadic logic with equality [36], which essentially adds to the modal one-step language the capability of counting elements of one-step models. It is precisely this capacity for counting that is the reason why formulas in this one-step language do not generally correspond to predicate liftings for the powerset functor, since conditions like “having at least two elements” is clearly not preserved by morphisms between one-step models. So we are looking for a uniform construction that prevents making any distinctions between one-step models by counting, and the solution is to create infinitely many copies of each element. This corresponds to the $\omega$-unravelling construction used by [13].

{defi}

We say that a one-step language $\mathtt{L}$ admits uniform translations if, for any finite set $A$ and any finite set $\Gamma$ of formulas in $\mathtt{L}(A)$, there exists a uniform construction $(-)_{*}$ and a translation $(-)^{*}:\Gamma\to\mathtt{1ML}_{\Lambda}(A)$ such that for any one-step model $(X,\alpha,V)$ and any $\varphi\in\Gamma$, we have

[TABLE]

where $h_{\alpha}$ is the cover assigned to $(X,\alpha)$ by the construction. The pair consisting of the translation $(-)^{*}$ and the uniform construction $(-)_{*}$ will be referred to as a uniform translation for the set of formulas $\Gamma$.

As an example, consider the disjunctive formulas introduced by Walukiewicz,

{defi}

Given a $P$-chromatic second-order automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ and a uniform translation for the finite set $\Delta[A\times\mathcal{P}(P)]$, we get a corresponding modal automaton $\mathbb{A}^{*}=(A,\Delta^{*},a_{I},\Omega)$, with $\Delta^{*}$ given by $\Delta^{*}(a,c)\mathrel{:=}(\Delta(a,c))^{*}$. We overload the notation $(\cdot)^{*}$ to refer both to a uniform one-step translation and the induced translation at the level of automata.

The proof of the following result closely follows that of the main result in [35]. The only difference with [35] is that here we need an “unravelling”-like component, in order to turn an arbitrary model into a tree-like one.

Proposition 31**.**

Assume that $\mathtt{1SO}_{\Lambda}$ admits uniform translations, and let $\mathbb{A}$ be a second-order $\Lambda$-automaton. Then for each pointed $\mathsf{T}$-model $(\mathbb{S},s)$ there is a $\mathsf{T}$-tree model $(\mathbb{T},R,t)$, with a $\mathsf{T}$-model morphism $f$ from $\mathbb{T}$ to $\mathbb{S}$, mapping $t$ to $s$, and such that

[TABLE]

Proof 5.1**.**

Consider any given pointed $\mathsf{T}$-model $(\mathbb{S}_{1},s_{1})$ where $\mathbb{S}_{1}=(S_{1},\sigma_{1},V_{1})$. We are going to construct a $\mathsf{T}$-tree model $(\mathbb{S}_{2},R,s_{2})$, $\mathbb{S}_{2}=(S_{2},\sigma_{2},V_{2})$, together with a model morphism from the underlying pointed $\mathsf{T}$-model $\mathbb{S}_{2}$ to $\mathbb{S}_{1}$ mapping $s_{2}$ to $s_{1}$, and such that $\mathbb{A}$ accepts the $\mathsf{T}$-tree model $(\mathbb{S}_{2},s_{2})$ if and only if $\mathbb{A}^{*}$ accepts the pointed $\mathsf{T}$-model $(\mathbb{S}_{1},s_{1})$.

We construct this $\mathsf{T}$-tree model as follows: for each $u\in S_{1}$, we define an associated pair $(X_{u},\alpha_{u})$ by setting $(X_{u},\alpha_{u})=((S_{1})_{*},\sigma_{1}(u)_{*})$. Observe that, by the construction of these one-step models, for each $u\in S_{1}$, there is a mapping $\xi_{u}:X_{u}\rightarrow S_{1}$ such that:

1. (1)

$\mathsf{T}(\xi_{u})(\alpha_{u})=\sigma_{1}(u)$** 2. (2)

For each valuation $U:A\rightarrow\mathcal{Q}(S_{1})$, every $u\in S_{1}$ and every one-step formula $\Delta(a,c)$ appearing in $\mathbb{A}$, we have

[TABLE]

The map $\xi_{u}$ is given by $h_{\sigma_{1}(u)}$. We now construct the $\mathsf{T}$-tree model $(S_{2},R,\sigma_{2},s_{2},V_{2})$ as follows: first, consider the set of all non-empty finite (non-empty) tuples $(v_{1},...,v_{n})$ of elements in

[TABLE]

such that $v_{1}=s_{1}$. We define, by induction, for each natural number $n>0$ a subset $M_{n}$ of this set, and a mapping $\gamma_{n}:M_{n}\rightarrow S_{1}$, as follows:

• •

Set $M_{1}=\{(s_{1})\}$, and define $\gamma_{1}(s_{1})=s_{1}$.

• •

Set $M_{n+1}=\{\vec{v}w\mid\vec{v}\in M_{n},w\in X_{\gamma_{n}(\vec{v})}\}$. Define $\gamma_{n+1}(\vec{v}w)=\xi_{\gamma_{n}(\vec{v})}(w)$.

Here, we write $\vec{v}w$ to denote the tuple $(v_{1},...,v_{n},w)$ if $\vec{v}=(v_{1},...,v_{n})$. Set $S_{2}=\bigcup_{n>0}M_{n}$, and define $\gamma=\bigcup_{n>0}\gamma_{n}$. Define the relation $R\subseteq S_{2}\times S_{2}$ to be

[TABLE]

Note that there is, for every $\vec{v}\in S_{2}$, a bijection $i_{\vec{v}}:X_{\gamma(\vec{v})}\to R(\vec{v})$ given by $w\mapsto\vec{v}w$. Note also that, for each $\vec{v}\in S_{2}$, we have

[TABLE]

With this in mind, we define the coalgebra structure $\sigma_{2}$ by setting

[TABLE]

Note that $\sigma_{2}(\vec{v})|_{R(\vec{v})}=\mathsf{T}i_{\vec{v}}(\alpha_{\gamma}(\vec{v}))$. Finally, set $s_{2}$ to be the unique singleton tuple with sole element $s_{1}$, and define the valuation $V_{2}$ by setting $V_{2}^{\dagger}(\vec{v})=V_{1}^{\dagger}(\gamma(\vec{v}))$.

Clearly, $(S_{2},R,\sigma_{2},s_{2},V_{2})$ is a $\mathsf{T}$-tree model. Denote the underlying $\mathsf{T}$-model by $\mathbb{S}_{2}$. We can then prove the following two claims:

Claim 32**.**

The map $\gamma$ is a $\mathsf{T}$-model morphism from $\mathbb{S}_{2}$ to $\mathbb{S}_{1}$.

Proof 5.2** (Proof of Claim 32).**

The map $\gamma$ clearly respects the truth values of all propositional atoms, and $\gamma(s_{2})=s_{1}$. It suffices to show that $\gamma$ is a coalgebra morphism, i.e. that $\mathsf{T}\gamma(\sigma_{2}(\vec{v}))=\sigma_{1}(\gamma(\vec{v}))$ for all $\vec{v}$. Pick any $\vec{v}\in S_{2}$. We have:

[TABLE]

as required.

Claim 33**.**

$\mathbb{A}$* accepts $(S_{2},R,\sigma_{2},s_{2},V_{2})$ iff $\mathbb{A}^{*}$ accepts $\mathbb{S}_{1}$.*

Proof 5.3** (Proof of Claim 33:).**

We have two parts that need to be proved here:

First part: $\mathbb{A}$ accepts $(S_{2},R,\sigma_{2},s_{2},V_{2})$ implies $\mathbb{A}^{*}$ accepts $(\mathbb{S}_{1},s_{1})$

Suppose that $\chi$ is a (positional) winning strategy in the acceptance game for $\mathbb{A}$ and $(S_{2},R,\sigma_{2},s_{2},V_{2})$. We are going to define a strategy $\chi^{*}$ for $\exists$ in the acceptance game for $\mathbb{A}^{*}$ and $\mathbb{S}_{1}$, with the property that for any $\chi^{*}$-guided partial match

[TABLE]

of length $n$ with $s^{i}_{i}\in S_{1}$ and $s_{1}^{1}=s_{1}$, there exists a $\chi$-guided partial match

[TABLE]

with $s^{2}_{i}\in S_{2}$, $s_{1}^{2}=s_{2}$ and $\gamma(s^{2}_{i})=s^{1}_{i}$ for each index $i$, and chosen in such a way that if a $\chi^{*}$-guided match $\rho^{\prime}$ is an extension of $\rho$, then the $\chi$-guided match $\rho^{\prime}_{*}$ is an extension of the $\chi$-guided match $\rho_{*}$.

We define the strategy $\chi^{*}$ by induction on the length of a partial match. For the partial match $\rho$ consisting of the single position $(a_{I},s^{1}_{1})$ we let $\rho_{*}$ consist of the single position $(a_{I},s_{2})$, and we define the valuation $\chi^{*}(\rho):A\rightarrow\mathcal{Q}(S_{1})$ by setting, for each $b\in A$,

[TABLE]

Similarly, suppose that $\chi^{*}$ has been defined for all matches of length less than $n$, and let $\rho$ be any match of length $n>1$. If $\rho$ is not $\chi^{*}$-guided, then we can define $\chi^{*}(\rho)(b)=\emptyset$ for all $b\in A$. If $\rho$ is $\chi^{*}$-guided, then write

[TABLE]

Since this match is $\chi^{*}$-guided, by the induction hypothesis there is a $\chi$-guided partial match

[TABLE]

with $\gamma(s^{2}_{i})=s^{1}_{i}$ for all $i$. We set, for each $b\in A$,

[TABLE]

Clearly, with this definition, the induction hypothesis continues to hold for all $\chi^{*}$-guided matches of length $n+1$. Furthermore, we note that, whenever $\rho$ is a $\chi^{*}$-guided match of length $n$, the move $\chi^{*}(\rho)$ is legal: since the move $\chi(a_{n},s^{2}_{n})$ must be legal, we have

[TABLE]

But since

[TABLE]

we see that $i_{s^{2}_{n}}$ is an isomorphism between the one-step models $(R[s^{2}_{n}],\sigma_{2}(s^{2}_{n})|_{R(s^{2}_{n})},\chi(a_{n},s^{2}_{n}))$ and $(X_{s^{1}_{n}},\alpha_{s^{1}_{n}},\chi(a_{n},s^{2}_{n})_{[i_{s^{2}_{n}}]})$, so we have

[TABLE]

For all $b\in A$, we have

[TABLE]

So by monotonicity we get

[TABLE]

Hence, since $\Delta^{*}(a_{n},V_{2}^{\dagger}(s^{2}_{n}))$ is the uniform translation of $\Delta(a_{n},V_{2}^{\dagger}(s^{2}_{n}))$, we get

[TABLE]

as required. It is now easy to show that $\exists$ never gets stuck in a $\chi^{*}$-guided partial match, and we also see that every infinite $\chi^{*}$-guided match

[TABLE]

corresponds to an infinite $\chi$-guided match

[TABLE]

and so since $\exists$ wins every infinite $\chi$-guided match, she wins every infinite $\chi^{*}$-guided match as well.

Second part: $\mathbb{A}^{*}$ accepts $(\mathbb{S}_{1},s_{1})$ implies $\mathbb{A}$ accepts $(S_{2},R,\sigma_{2},s_{2},V_{2})$

Let $\chi^{*}$ be a winning strategy for $\exists$ in the acceptance game for $\mathbb{A}^{*}$ and $\mathbb{S}_{1}$. We define the strategy $\chi$ as follows: given a partial match

[TABLE]

set $\chi(\rho)=\chi^{*}(\gamma(\rho))_{[\gamma]}$, where $\gamma(\rho)$ is the match

[TABLE]

It is straightforward to check that, whenever $\rho$ is a $\chi$-guided match, $\gamma(\rho)$ is a $\chi^{*}$-guided match, and that the move $\chi^{*}(\gamma(\rho))$ is legal if and only if the move $\chi(\rho)$ is legal. It follows that $\exists$ never gets stuck in a $\chi$-guided partial match, and that she wins every infinite $\chi$-guided match, since an infinite $\chi$-guided match

[TABLE]

corresponds to an infinite $\chi^{*}$-guided match

[TABLE]

*This concludes the proof.

The lemma now follows by combining the two claims 32 and 33. *

From this, we get the following result. Here, we use the fact that every $\mathtt{MSO}_{\Lambda}$-formula is equivalent to a monotone second-order automaton over $\mathsf{T}$-tree models, so that it suffices to find translations of monotone one-step formulas.

Theorem 34** (Auxiliary Characterization Theorem).**

Let $\Lambda$ be an expressively complete set of monotone predicate liftings for a set functor $\mathsf{T}$, and assume that the monotone fragment of the one-step language $\mathtt{1SO}_{\Lambda}$ admits uniform translations. Then:

[TABLE]

Proof 5.4**.**

Given a bisimulation invariant formula $\varphi$ of $\mathtt{MSO}_{\Lambda}$, let $\mathbb{A}$ be an equivalent monotone second-order automaton, and suppose there is a uniform translation $(-)^{*}$ of the monotone fragment of the one-step language $\mathtt{1SO}_{\Lambda}$. Let $\psi$ be a formula in $\mu\mathtt{ML}_{\Lambda}$ equivalent to the automaton $\mathbb{A}^{*}$. Then for any pointed $\mathsf{T}$-model $\mathbb{S},s$, let $(\mathbb{T},R,t)$ be the $\mathsf{T}$-tree model provided by Proposition 31. Then we get:

[TABLE]

and the proof is done.

5.2. Adequate uniform constructions

The existence of uniform translations for the one-step language [35] involves two components: a translation on the syntactic side and a uniform construction on the semantic side. One of our main new observations in this paper is that we can actually forget about the syntactic translation and focus entirely on the model-theoretic side of the construction. If we can find a suitable uniform construction for the one-step models, satisfying a certain model-theoretic condition with respect to the second-order one-step language, the syntactic translation will come for free.

{defi}

Let $\varphi$ be any one-step formula in $\mathtt{1SO}_{\Lambda}(A)$. Then a uniform construction $(-)_{*}$ for $\mathsf{T}$ is called adequate for $\varphi$ if, for any pair of one-step frames $(X,\alpha)$ and $(Y,\beta)$, any one-step frame morphism $f:(X,\alpha)\rightarrow(Y,\beta)$ and any valuation $V:A\rightarrow\mathcal{Q}(Y)$, we have the following condition $(\star)$:

[TABLE]

where $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ and $h_{\beta}:(Y_{*},\beta_{*})\to(Y,\beta)$ are the covering maps given by the uniform construction. We say that the construction is adequate for a set of formulas $\Gamma$ if it is adequate for every member of $\Gamma$.

The following diagram clarifies condition $(\star)$:

[TABLE]

We are now ready to prove our first main theorem, stating that if $\mathsf{T}$ admits an adequate construction for any finite set of one-step formulas, then $\mathtt{MSO}_{\mathsf{T}}/{\sim}\equiv\mu\mathtt{ML}_{\mathsf{T}}$.

Proof 5.5** (Proof of Theorem 2).**

By Theorem 34 it suffices to show that the monotone fragment of $\mathtt{1SO}_{\mathsf{T}}$ admits uniform translations. Let $\Gamma$ be a finite set of monotone formulas of $\mathtt{1SO}_{\mathsf{T}}(A)$, for some finite set $A$, and suppose the uniform construction $(-)_{*}$ is adequate for $\Gamma$. Given $\varphi\in\Gamma$ we define a monotone predicate lifting $\lambda$ over $A$ by setting

[TABLE]

It is easy to check that this lifting is monotone, and naturality of $\lambda$ is a direct consequence of the condition $(\star)$. If $A$ has $n$ elements and we list these as $(a_{1},...,a_{n})$, then we can view $\lambda$ as a formula in $\mathtt{1ML}_{\Lambda}(A)$ of the form $\lambda^{\prime}(a_{1},...,a_{n})$, where $\lambda^{\prime}$ is the $n$-place predicate lifting corresponding to $\lambda$ with this given ordering of $A$. We now get a uniform translation by mapping $\varphi$ to the formula $\lambda^{\prime}(a_{1},...,a_{n})$.

Note that, if $\Lambda$ is an expressively complete set of liftings for $\mathsf{T}$, then it suffices to find an adequate uniform construction for every finite set of formulas in $\mathtt{1SO}_{\Lambda}(A)$, since every formula in $\mathtt{1SO}_{\mathsf{T}}(A)$ is semantically equivalent to one in $\mathtt{1SO}_{\Lambda}(A)$. Hence, by Theorem 34 we get:

Corollary 35**.**

Let $\mathsf{T}$ be any set functor, and let $\Lambda$ be an expressively complete set of predicate liftings for $\mathsf{T}$. If $\mathsf{T}$ admits an adequate uniform construction for every finite set of formulas of $\mathtt{1SO}_{\Lambda}$, then

[TABLE]

If $\mathsf{T}$ preserves weak pullbacks then we can reformulate $(\star)$ as the following condition: {defi} Suppose $\mathsf{T}$ preserves weak pullbacks. A one-step $\overline{\mathsf{T}}$-bisimulation between one-step models $(X,\alpha,V)$ and $(Y,\beta,U)$ is a relation $R\subseteq X\times Y$ such that:

• •

If $xRy$ then $V^{\dagger}(x)=U^{\dagger}(y)$.

• •

$(\alpha,\beta)\in\overline{\mathsf{T}}R$.

Proposition 36**.**

Suppose that $\mathsf{T}$ preserves weak pullbacks, and let $(-)_{*}$ be a uniform construction for $\mathsf{T}$. Then $(-)_{*}$ is adequate for $\varphi$ if, and only if, for every pair of one-step $\overline{\mathsf{T}}$-bisimilar one-step models $(X,\alpha,V)$ and $(Y,\beta,U)$ we have:

[TABLE]

5.3. Some easy applications

We now start with some straightforward applications of the main characterization theorem.

{exa}

As a first application, the standard Janin-Walukiewicz characterization of the modal $\mu$-calculus can be seen as an instance of the first main characterization result by taking $\Lambda=\{\Diamond\}$ and $\mathsf{T}=\mathcal{P}$, recalling that $\mathtt{MSO}=\mathtt{MSO}_{\{\Diamond\}}$. The uniform construction for $\mathcal{P}$, which is adequate with respect to any set of one-step formulas, is given as follows: consider a pair $(X,\alpha)$ with $\alpha\in\mathcal{P}(X)$. We take this to $X_{*}=\alpha_{*}=\alpha\times\omega$, and we let $h_{\alpha}:\alpha\times\omega\to X$ be the projection map. Proving adequacy of this construction is an exercise in model theory, and left to the reader. (The proof is a much simpler special case of the argument we will use in Section 6.2.)

{exa}

Consider the finitary multiset (“bags”) functor $\mathcal{B}$, which sends a set $X$ to the set of mappings $f:X\rightarrow\omega$ such that the set $\{u\in X\mid f(u)=0\}$ is cofinite. The action on morphisms is given by letting, for $f\in\mathcal{B}X$ and $h:X\rightarrow Y$, the multiset $\mathcal{B}h(f):Y\rightarrow\omega$ be defined by $w\mapsto\sum_{h(v)=w}f(v)$. Given a pair $X,\alpha$ where $\alpha:X\rightarrow\omega$ has finite support, we define

[TABLE]

Here, we follow the standard procedure and identify each finite ordinal $n\in\omega$ with the set of smaller ordinals, so that [math] is identified with $\emptyset$, $1$ is $\{\emptyset\}$, $2$ is $\{\emptyset,\{\emptyset\}\}$ and so on. The mapping $\alpha_{*}:X_{*}\rightarrow\omega$ is defined by setting $\alpha_{*}(w)=1$ for all $w\in X_{*}$. The map $h_{\alpha}:X_{*}\rightarrow X$ is defined by $(u,i)\mapsto u$. It is easy to check that whenever two one-step frames $(X,\alpha)$ and $(Y,\beta)$ are related by some morphism $f:(X,\alpha)\to(Y,\beta)$, the models $(X_{*},\alpha_{*},V_{[f\circ h_{\alpha}]})$ and $(Y_{*},\beta_{*},V_{[h_{\beta}]})$ are isomorphic, for any valuation $V:A\to\mathcal{Q}(Y)$. It follows that the construction is adequate for any set of one-step formulas, hence we get $\mu\mathtt{ML}_{\mathcal{B}}\equiv\mathtt{MSO}_{\mathcal{B}}{/}{\sim}$.

{exa}

Consider the set of all exponential polynomial functors [12] defined by the “grammar”:

[TABLE]

where $\mathsf{C}$ is any constant functor for some set $C$, and $\mathsf{Id}$ is the identity functor on $\mathbf{Set}$. These functors cover many important applications: streams, binary trees, deterministic finite automata and deterministic labelled transition systems are all examples of coalgebras for exponential polynomial functors, as is the so called game functor whose coalgebras provide semantics for Coalition Logic [5]. For this last instance, the “game functor” $\mathcal{G}$ for $n$ agents can be written in the form of an exponential polynomial functor as follows:

[TABLE]

Then, for a given set $X$, an element of $\mathcal{G}X$ will be a pair consisting of a vector $\langle S_{0},...,S_{n-1}\rangle$ of available strategies for each player, together with an “outcome map” $f$ assigning an element of $X$ to each strategy profile in $S_{0}\times...\times S_{n-1}$.

Every exponential polynomial functor admits adequate uniform constructions for all sets of one-step formulas. The proof proceeds by a straighforward induction, and similarly to the case for the bags functor it provides each exponential polynomial functor $\mathsf{T}$ with a uniform construction such that for any one-step frame morphism $f:(X,\alpha)\to(Y,\beta)$ and any $V:A\to\mathcal{Q}(Y)$, the one-step models $(X_{*},\alpha_{*},V_{[f\circ h_{\alpha}]})$ and $(Y_{*},\beta_{*},V_{[h_{\beta}]})$ are isomorphic. Hence, we get:

Theorem 37**.**

For every exponential polynomial functor $\mathsf{T}$, we have $\mu\mathtt{ML}_{\mathsf{T}}\equiv\mathtt{MSO}_{\mathsf{T}}{/}{\sim}$.

Proof 5.6**.**

We provide a sketch of the inductive construction of an adequate uniform construction.

Constant functor

For the constant functor $\mathsf{C}$, a one-step frame is a pair $(X,c)$ with $c\in C$. We set $X_{*}=\emptyset$, $c_{*}=c$ and $h_{c}:\emptyset\to X$ to be the unique inclusion of the empty set.

Identity functor

Given a one-step frame $(X,u)$ for the identity functor, which consists of a set $X$ and $u\in X$, we set $X_{*}=\{u\}$, $u_{*}=u$ and we set $h_{u}:\{u\}\to X$ to be the inclusion map sending $u$ to itself.

Product

Suppose that $\mathsf{T}_{1}$ and $\mathsf{T}_{2}$ have associated adequate uniform constructions with the required property. Consider a one-step $\mathsf{T}_{1}\times\mathsf{T}_{2}$-frame $(X,(\alpha,\beta))$ with $\alpha\in\mathsf{T}_{1}X$ and $\beta\in\mathsf{T}_{2}X$. Let $h_{1}:(X_{1},\alpha_{1})\to(X,\alpha)$ be the cover assigned by the uniform construction for $\mathsf{T}_{1}$ and let $h_{2}:(X_{2},\beta_{2})\to(X,\beta)$ be the cover assigned by the uniform construction for $\mathsf{T}_{2}$. Then we take $X_{*}$ to be the disjoint union $X_{1}+X_{2}$, and set

[TABLE]

where $i_{1}:X_{1}\to X_{1}+X_{2}$ and $i_{2}:X_{2}\to X_{1}+X_{2}$ are the insertion maps for the co-product. Finally, we define the covering map $h_{(\alpha,\beta)}:X_{1}+X_{2}\to X$ be obtained by simply co-tupling the maps $h_{1},h_{2}$, i.e. $h_{(\alpha,\beta)}$ is the map given by the universal property of the co-product applied to the diagram $X_{1}\stackrel{{\scriptstyle h_{1}}}{{\longrightarrow}}X\stackrel{{\scriptstyle h_{2}}}{{\longleftarrow}}X_{2}$. We get:

[TABLE]

so $h_{(\alpha,\beta)}$ is indeed a covering map as required.

Exponentiation

The case of a functor $\mathsf{T}^{\mathsf{C}}$ for some constant $\mathsf{C}$ is handled analogously with the case of binary products, so we leave it to the reader.

Co-product

*This step of the construction is actually the easiest one. Suppose that each functor $\mathsf{T}_{i}$ for $i\in I$ is equipped with an adequation uniform construction, in the strong sense demanded by our induction hypothesis. Without loss of generality let’s assume that $\mathsf{T}_{i}X\cap\mathsf{T}_{j}X=\emptyset$ for $i\neq j$. Let $(X,\alpha)$ be a one-step frame for the co-product $\coprod_{i\in I}\mathsf{T}_{i}$. Then there is a unique $i\in I$ with $\alpha\in\mathsf{T}_{i}X$, and so we define the cover $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ merely by applying the uniform construction for $\mathsf{T}_{i}$. *

Remark 38**.**

These uniform constructions were all designed in a case-by-case fashion, and at the present time we do not know whether there is any general recipe for producing an adequate uniform construction when it exists. What the constructions mentioned so far seem to have in common is that we want to produce as many equivalent (in some sense) copies of each state in a one-step model, but this is not always sufficient. In the next section we will see a somewhat more involved construction for the monotone mu-calculus, which aims to create sufficiently many copies of each state but also, crucially, sufficiently many pairwise disjoint copies of all the neighborhoods. In this case we are trying to neutralize not only the capability of the second-order one-step language to count states in one-step models, but also its capability to express how certain neighborhoods are related to each other, in particular, whether they overlap or not. For example, the second-order one-step language can express the property that any two neighborhoods intersect, or there is a smallest neighborhood contained in all others etc., and the uniform construction we provide needs to trivialize all such statements. In general, applying our main result as it stands may require a bit of creativity, and we regard it as an interesting (possibly quite hard) task for future research to come up with a result that makes the task entirely mechanical. We mention some related questions in our concluding remarks section.

6. Characterizing the monotone $\mu$-calculus

This final section of the paper concerns the monotone neighborhood functor $\mathcal{M}$. There are two main difficulties here. First, the uniform construction will be less straightforward than in the previous applications, for the reasons that we explained above. Second, we need to do a bit of “pre-processing” of the monotone neighborhood functor to make the technique of uniform constructions applicable. In fact, the characterization theorem cannot possibly apply directly to the monotone $\mu$-calculus: it turns out that there is no adequate uniform construction for $\mathcal{M}$. For these reasons, we view the results of this section as an independent contribution of the paper, rather than just another application to illustrate the main theorem.

Proposition 39**.**

The functor $\mathcal{M}$ does not admit an adequate uniform construction for the formula $\varphi$ defined as: $\neg\mathsf{Em}(a)$.

Proof 6.1**.**

The formula $\varphi$ just says that the value of $a$ is non-empty. Suppose there existed an adequate uniform construction for this formula. Consider the situation depicted in the diagram below, which shows three one-step frames together with two one-step frame morphisms, one for each of the two bottom one-step frames. The top frame consists of two points $\{w_{1},w_{2}\}$ and has neighborhoods $\{\{w_{1},w_{2}\},\{w_{2}\}\}$, the bottom left frame has points $\{u_{1},u_{2},u_{3}\}$ and neighborhoods $\{\{u_{1},u_{2}\},\{u_{2},u_{3}\},\{u_{1},u_{2},u_{3}\}\}$. Finally the bottom right frame has a single point $\{v\}$ and this singleton as its only neighborhood. In other words, the picture shows a co-span in the category of one-step frames and one-step frame morphisms. Furthermore, consider the valuation on the topmost one-step frame which makes $a$ true at exactly the one state $w_{1}$, i.e. the one not belonging to the singleton neighborhood. This valuation is depicted in the diagram by representing the state where $a$ is true by a blank circle, and the state where it is not true by a filled circle. The induced valuations on the bottom one-step frames via the frame morphisms are depicted in the same manner. With respect to these valuations, $p$ will be true at $u_{1}$, but false at $u_{2},u_{3}$ and $v$.

Every cover satisfies $\varphi$No cover satisfies $\varphi$

Let us denote the top frame by $(Y,\beta)$, its valuation by $V$, the bottom-left frame as $(X,\alpha)$, the bottom-right one as $(X^{\prime},\alpha^{\prime})$ and the corresponding frame morphisms as $f$ and $f^{\prime}$ respectively. Now, the supposed adequate construction will assign a cover to each of the three frames, and we get valuations for each cover from the valuations depicted in the diagram. It follows from the defining condition $(\star)$ for adequacy that $\varphi$ must have the same truth value in each of these covers. But this leads to a contradiction: it is not hard to check that the cover $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ must be such that $(X_{*},\alpha_{*},V_{[f\circ h_{\alpha}]})\Vdash\varphi$, because the image of the map $h_{\alpha}$ must support $\alpha$ and therefore include the one element of $X$ coloured red. On the other hand, we clearly must have $(X^{\prime}_{*},\alpha^{\prime}_{*},V_{[f^{\prime}\circ h_{\alpha^{\prime}}]})\nvDash\varphi$, which contradicts the condition $(\star)$.

6.1. The supported companion of a functor

Our solution to the problem we are facing with the monotone neighborhood functor is to perform a gentle repair, changing the functor into a closely related one that does admit an adequate uniform construction. The construction has some independent interest from a general coalgebraic perspective, so we define it in general terms: {defi} The supported companion $\underline{\mathsf{T}}$ of a set functor $\mathsf{T}$ is the sub-functor of $\mathcal{P}\times\mathsf{T}$ defined by:

[TABLE]

It is easy to check that this is indeed a well-defined subfunctor of $\mathcal{P}\times\mathsf{T}$, since for any map $f:X\to Y$, any $\alpha\in\mathsf{T}X$ and any set $Z\subseteq X$, the image $f[Z]=\mathcal{P}f(Z)$ is a support for $\mathsf{T}f(\alpha)$ whenever $Z$ is a support for $\alpha$. The reader may also note that what we have called “$\mathsf{T}$-tree models” are actually special instances of $\underline{\mathsf{T}}$-models, so in a sense the supported companion functor has already played a role in the proof of the main theorem. We will show that this construction repairs the monotone neighborhood functor, so that the supported companion $\underline{\mathcal{M}}$ of $\mathcal{M}$ admits an adequate uniform construction. Interestingly enough, the same construction happens to repair weak pullback preservation:

Proposition 40**.**

The functor $\underline{\mathcal{M}}$ preserves weak pullbacks.

We leave the verification of this to the reader; the argument is similar to the reasoning in [20] used to establish the existence of a well-behaved relation lifting for $\mathcal{M}$.

Note that we have an obvious natural transformation $\pi:\underline{\mathsf{T}}\to\mathcal{P}$ with components given by the projection maps sending $(Z,\alpha)\in\underline{\mathsf{T}}X$ to $Z\in\mathcal{P}(X)$, and we can compose this with the predicate lifting $\Box:\mathcal{Q}\to\mathcal{Q}\circ\mathcal{P}$ to obtain a predicate lifting $\underline{\Box}$ for $\underline{\mathsf{T}}$ defined by:

[TABLE]

We call this lifting the support modality for $\underline{\mathsf{T}}$, and write its dual as $\underline{\Diamond}$. Furthermore, any lifting $\lambda$ for $\mathsf{T}$ corresponds to a lifting for $\underline{\mathsf{T}}$ by composing $\lambda$ with the projection from $\underline{\mathsf{T}}$ to $\mathsf{T}$ in the same manner, and we will not take care to distinguish $\lambda$ as a lifting for $\mathsf{T}$ from the corresponding lifting for $\underline{\mathsf{T}}$. A little issue that we need to address, before we can proceed to characterize the monotone $\mu$-calculus, is just how the language $\mathtt{\mu ML}_{\Lambda}$ is related to $\mathtt{\mu ML}_{\Lambda\cup\{\underline{\Box}\}}$ for a given set of liftings $\Lambda$ for $\mathsf{T}$. The rest of this subsection will provide the answer, and give a characterization theorem for $\mathtt{\mu ML}_{\Lambda}$ as the $\mathsf{T}$-bisimulation invariant fragment of $\mathtt{\mu ML}_{\Lambda\cup\{\underline{\Box}\}}$, where a formula is said to be $\mathsf{T}$-bisimulation invariant if it has the same truth value in any two pointed $\underline{\mathsf{T}}$-models for which the corresponding $\mathsf{T}$-models are behaviourally equivalent. Formally we shall write $(\mathbb{S},s)\sim(\mathbb{S}^{\prime},s^{\prime})$, for $\underline{\mathsf{T}}$-models $\mathbb{S}$ and $\mathbb{S}^{\prime}$, to say that the respective underlying pointed $\mathsf{T}$-models are behaviourally equivalent. To distinguish this from actual behavioural equivalence in the sense of the companion functor $\underline{\mathsf{T}}$, we write $(\mathbb{S},s)\;\underline{\sim}\;(\mathbb{S}^{\prime},s^{\prime})$ to say that these pointed models are behaviourally equivalent as $\underline{\mathsf{T}}$-models.

We borrow a result from [8]:

Fact 41** ([8]).**

For any set of liftings $\Lambda$ for any set functor $\mathsf{T}$, the logic $\mu\mathtt{ML}_{\Lambda}$ has the finite model property.

We assume that we have at our disposal a fixed $\underline{\mathsf{T}}$-model $\mathbb{U}=(U,\gamma,V)$ which is a disjoint union of one isomorphic copy for every finite pointed $\underline{\mathsf{T}}$-model $(\mathbb{S},s)$. It is not hard to see that such a model does exist: just take a disjoint union containing each $\underline{\mathsf{T}}$-model defined on some finite subset $n=\{0,...,n-1\}$ of $\omega$. Since the class of all these models clearly forms a set, their disjoint union is a well defined $\underline{\mathsf{T}}$-model.

{defi}

Let $\mathbb{S}$ be any finite $\underline{\mathsf{T}}$-model. We define the model $\mathbb{S}\oplus\mathbb{U}=(S+U,\sigma_{+},V_{+})$ such that, for each $s\in S$ we have

[TABLE]

where $\sigma(s)=(X,\alpha)$, and for $u\in U$ we have $\sigma_{+}(u)=\underline{\mathsf{T}}\iota_{U,S+U}(\gamma(u))$555In this definition we have used “$+$” as the symbol for binary coproducts of sets..

Note that the underlying $\mathsf{T}$-model of $\mathbb{S}\oplus\mathbb{U}$ is just the co-product of the underlying $\mathsf{T}$-models of $\mathbb{S}$ and $\mathbb{U}$ respectively.

The following lemmas are immediate from the definition.

Lemma 42**.**

Let $\mathbb{S}$ be any $\underline{\mathsf{T}}$-model. Then for all $u\in U$, we have:

[TABLE]

Lemma 43**.**

For any $\mathsf{T}$-model $\mathbb{S}$ and $s\in S$: $(\mathbb{S},s)\sim(\mathbb{S}\oplus\mathbb{U},s)$.

Note that Lemma 43 is not guaranteed to hold if we replace $\sim$ by the finer equivalence relation $\underline{\sim}$.

It will be convenient in this section to work with a second version of the acceptance game for a modal $\Lambda$-automaton or a modal $\Lambda\cup\{\underline{\Box}\}$-automaton, which we will call the extended acceptance game for $\mathbb{A}$ with respect to a model $\mathbb{S}$, denoted $\mathcal{E}(\mathbb{A},\mathbb{S})$. Given a modal $\Lambda$-automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ and a model $\mathbb{S}=(S,\sigma,V)$ this game has three types of positions: pairs of the form $(\psi,s)$ with $\psi\in\mathtt{1ML}_{\Lambda}(A)$, pairs of the form $(\psi,s)$ with $\psi\in\mathtt{Latt}(A)$ (lattice formulas over $A$, as defined in Definition 3.3), and maps $f:\mathtt{Latt}(A)\to\mathcal{P}(S)$. Admissible moves are given in Table 4:

Here, $\lambda\in\Lambda\cup\{\underline{\Box}\}$. It is easy to see that the position $(\top,s)$ is always winning for $\exists$, and $(\bot,s)$ is always winning for $\forall$. The following result is entirely routine to prove:

Theorem 44**.**

Let $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ be a modal $\Lambda$-automaton and $(\mathbb{S},s)$ a pointed $\mathsf{T}$-model. Then $\mathbb{A}$ accepts $(\mathbb{S},s)$ if, and only if, $(a_{I},s)$ is a winning position in the extended acceptance game.

We also have the following observation:

Proposition 45**.**

Let $\psi$ be any one-step formula in $\mathtt{1ML}_{\Lambda}(A)$ for a set of liftings $\Lambda$ for some given set functor $\mathsf{T}$, and let $\mathsf{P}\in\{\forall,\exists\}$. If $(\mathbb{S},s)\;\underline{\sim}\;(\mathbb{S}^{\prime},s^{\prime})$ then the position $(\psi,s)$ is winning for $\mathsf{P}$ in $\mathcal{E}(\mathbb{A},\mathbb{S})$ if and only if $(\psi,s^{\prime})$ is a winning position for $\mathsf{P}$ in $\mathcal{E}(\mathbb{A},\mathbb{S}^{\prime})$.

This means that for a pair of $\underline{\mathsf{T}}$-models $\mathbb{S}$ and $\mathbb{S}^{\prime}$ such that $(\mathbb{S},s)\;\underline{\sim}\;(\mathbb{S}^{\prime},s^{\prime})$, and a formula $\psi\in\mathtt{ML}_{\Lambda\cup\{\underline{\Box}\}}^{1}(A)$, the position $(\psi,s)$ is winning for $\mathsf{P}$ in $\mathcal{E}(\mathbb{A},\mathbb{S})$ if and only if $(\psi,s^{\prime})$ is a winning position for $\mathsf{P}$ in $\mathcal{E}(\mathbb{A},\mathbb{S}^{\prime})$. {defi} Let $\mathbb{A}=(A,\Delta,a_{I},\Omega)$ be a $\Lambda\cup\{\underline{\Box}\}$-automaton and let $\psi$ be a formula in the range of $\Delta$. We say that $\psi$ is $\mathbb{A}$-valid if for all (finite) pointed $\mathsf{T}$-models $(\mathbb{S},s)$, the position $(\psi,s)$ is winning in $\mathcal{E}(\mathbb{A},\mathbb{S})$. We say that $\psi$ is $\mathbb{A}$-satisfiable if there is some (finite) pointed $\mathsf{T}$-model $(\mathbb{S},s)$, the position $(\psi,s)$ is winning in $\mathcal{E}(\mathbb{A},\mathbb{S})$.

Let $\Lambda$ be any set of predicate liftings for $\mathsf{T}$ and let $\mathbb{A}$ be any modal $\Lambda\cup\{\underline{\Box}\}$-automaton. Making use of our fixed $\underline{\mathsf{T}}$-model $\mathbb{U}$ we shall define a translation $t_{\mathbb{A}}:\mathtt{1ML}_{\Lambda\cup\{\underline{\Box}\}}(A)\to\mathtt{1ML}_{\Lambda}(A)$ by induction as follows:

• •

For $\lambda\in\Lambda$, we set $t_{\mathbb{A}}(\lambda(\psi_{1},...,\psi_{k}))=\lambda(\psi_{1},...,\psi_{k})$, and similarly for the dual $\lambda^{d}$ for every lifting $\lambda\in\Lambda$.

• •

$t_{\mathbb{A}}(\top)=\top$ and $t_{\mathbb{A}}(\bot)=\bot$.

• •

$t_{\mathbb{A}}(\psi_{1}\vee\psi_{2})=t_{\mathbb{A}}(\psi_{1})\vee t_{\mathbb{A}}(\psi_{2})$ and $t_{\mathbb{A}}(\psi_{1}\wedge\psi_{2})=t_{\mathbb{A}}(\psi_{1})\wedge t_{\mathbb{A}}(\psi_{2})$.

• •

t_{\mathbb{A}}(\underline{\Box}\psi)=\left\{\begin{array}[]{ll}\top&\text{ if \psi$is$\mathbb{A}-valid }\\ \bot&\text{ otherwise }\end{array}\right\}.

• •

t_{\mathbb{A}}(\underline{\Diamond}\psi)=\left\{\begin{array}[]{ll}\top&\text{ if \psi$is$\mathbb{A}-satisfiable}\\ \bot&\text{ otherwise }\end{array}\right\}.

Note that this translation depends on the whole automaton $\mathbb{A}$, not just the set of variables $A$. So for any given set of variables $A$, we have one translation $t_{\mathbb{A}}:\mathtt{1ML}_{\Lambda\cup\{\underline{\Box}\}}(A)\to\mathtt{1ML}_{\Lambda}(A)$ for each automaton $\mathbb{A}$ with states $A$, and the translations will generally be different for different choices of $\mathbb{A}$. However, we will drop the index $\mathbb{A}$ from now on to simplify notation. Given a modal $\Lambda\cup\{\underline{\Box}\}$-automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega)$, we will write $t(\mathbb{A})$ for the automaton $(A,\Delta^{t},a_{I},\Omega)$ where $\Delta^{t}$ is defined by $\Delta^{t}(a,c)=t(\Delta(a,c))$, where it is understood that $t$ denotes the translation $t_{\mathbb{A}}$. Clearly $t(\mathbb{A})$ is a modal $\Lambda$-automaton.

We shall view the translation $t$ as a map defined on the entire domain $\mathtt{1ML}_{\Lambda\cup\{\underline{\Box}\}}(A)\cup\mathtt{Latt}(A)$ by setting $t(\psi)=\psi$ for $\psi\in\mathtt{Latt}(A)$.

Lemma 46**.**

For every finite pointed model $(\mathbb{S},s)$, and for any modal $\Lambda\cup\{\underline{\Box}\}$-automaton $\mathbb{A}$, we have

[TABLE]

Proof 6.2**.**

For left to right, suppose that $(\mathbb{S},s)\Vdash t(\mathbb{A})$. By Theorem 44 there is a strategy $\chi$ for $\exists$ in the extended acceptance game for $t(\mathbb{A})$ and $\mathbb{S}$ which is winning at $(a_{I},s)$. Without loss of generality we may assume that $\chi$ is positional, and a winning strategy at every winning position in $\mathcal{E}(t(\mathbb{A}),\mathbb{S})$. Our goal is to construct a positional strategy $\chi^{\prime}$ for $\exists$ in the extended acceptance game for $\mathbb{A}$ and $\mathbb{S}\oplus\mathbb{U}$, which prescribes a move for $\exists$ at every position $(\psi,v)$ belonging to $\exists$ and with $v\in S$, such that:

1. (1)

$\chi^{\prime}$* assigns a legitimate move to every position belonging to $\exists$ of the form $(\psi,v)$ with $v\in S$ such that $(t(\psi),v)$ is a winning position in $\mathcal{E}(t(\mathbb{A}),\mathbb{S})$,* 2. (2)

every $\chi^{\prime}$-guided partial match $\rho$ starting at $(a_{I},s)$ and ending with a position $(\psi,v)$ satisfies one of the following two criteria:

**a: **

$v\in S$* and $t[\rho]$ is a $\chi$-guided match in $\mathcal{E}(t(\mathbb{A}),\mathbb{S})$ (hence consists only of winning positions for $\exists$).*

**b: **

$(\psi,v)$* is a winning position in $\mathcal{E}(\mathbb{A},\mathbb{S}\oplus\mathbb{U})$.*

Here, given that $\rho=\pi_{1}....\pi_{n}$, we define $t[\rho]=t(\pi_{1})....t(\pi_{n})$ where $t(\psi,v)=(t(\psi),v)$ if $\psi\in\mathtt{1ML}_{\Lambda}(A)\cup\mathtt{Latt}(A)$, and $t(f)=f$ for a position $f:\mathtt{Latt}(A)\to\mathcal{P}(S)$. Clearly, we can build a winning strategy in $\mathcal{E}(\mathbb{A},\mathbb{S}\oplus\mathbb{U})$ from such a strategy $\chi^{\prime}$.

We define the strategy $\chi^{\prime}$ by a case distinction, given a position $(\psi,v)$ belonging to $\exists$ with $v\in S$. If $\psi=\alpha_{1}\vee\alpha_{2}$ then $t(\psi)=t(\alpha_{1})\vee t(\alpha_{2})$, so we set $\chi^{\prime}(\psi,v)=(\alpha_{i},v)$ where $i$ is chosen so that $\chi(t(\psi),v)=(t(\alpha_{i}),v)$. If $\psi=\lambda(\varphi_{1},...,\varphi_{n})$ then $t(\psi)=\lambda(\varphi_{1},...,\varphi_{n})$ too, so we set $\chi^{\prime}(\psi,v)=\chi(t(\psi),v)$. A simple naturality argument shows that this is still a legitimate move in $\mathcal{E}(\mathbb{A},\mathbb{S}\oplus\mathbb{U})$.

Finally, the interesting case is the one involving the support modality: at a position $(\underline{\Diamond}\varphi,v)$, if $(t(\underline{\Diamond}\varphi),v)$ is winning for $\exists$ in $\mathcal{E}(\mathbb{A},\mathbb{S})$ then we must have $t(\underline{\Diamond}\varphi)=\top$, hence $\varphi$ is $\mathbb{A}$-satisfiable. Hence, by the construction of $\mathbb{U}$, and by Observation 45 there is some $u\in U$ such that $(\varphi,u)$ is winning for $\exists$ in $\mathcal{E}(\mathbb{A},\mathbb{S}\oplus\mathbb{U})$. So we let the strategy $\chi^{\prime}$ pick the position $(\varphi,u)$. For the case involving the dual $\underline{\Box}$, if $t(\underline{\Box}\varphi)=\top$ then $\varphi$ is valid, and we can let $\exists$ pick the map sending $\varphi$ to $S+U$.

We also need to check that every $\chi^{\prime}$-guided partial match satisfies one of the conditions (a) or (b), and we prove this by an induction on the length of a partial match. The only interesting case is for the extension of a partial match $\rho$ ending with a position $(\underline{\Box}\varphi,v)$. By the induction hypothesis on $\rho$, we have $v\in S$ and $(t(\underline{\Box}\varphi),v)$ is winning for $\exists$, hence we must have $t(\underline{\Box}\varphi)=\top$. This means that $\varphi$ is $\mathbb{A}$-valid, so any move $(\varphi,w)$ by $\forall$ answering the move $S+U$ by $\exists$ will satisfy the condition (b), i.e. $(\varphi,w)$ is winning for $\exists$ in $\mathcal{E}(\mathbb{A},\mathbb{S}\oplus\mathbb{U})$.

For right to left, suppose that $\exists$ has a winning strategy $\chi$ at the position $(a_{I},s)$ in the extended acceptance game for $\mathbb{A}$ with respect to $\mathbb{S}\oplus\mathbb{U}$. We shall give $\exists$ a winning strategy $\chi^{\prime}$ at the same position in the game for $t(\mathbb{A})$ with respect to $\mathbb{S}$. We shall inductively associate with every $\chi^{\prime}$-guided partial match $\pi$ of length $k$ a $\chi$-guided “shadow match” $(\psi_{1},v_{1}),...,(\psi_{k},v_{k})$ such that $\pi$ is of the form

[TABLE]

We shall also make sure that whenever $\pi^{\prime}$ is an extension of $\pi$, the shadow match associated with $\pi^{\prime}$ is an extension of the shadow match associated with $\pi$ as well. It will clearly follow that $\exists$ wins every infinite $\chi^{\prime}$-guided match.

For the singleton match consisting of $(a_{I},s)$ we let $(a_{I},s)$ itself be the shadow match. (This is acceptable because, by convention, we have set $t(a_{I})=a_{I}$.) For a match $\pi$ of length $k$ we define the move $\chi^{\prime}(\pi)$ depending on the shape of the last position on the associated shadow match. Again we treat only the interesting cases.

If the last position on the shadow match is $(\lambda(\psi_{1},...,\psi_{m}),v)$ then $\chi$ provides a map $f:\mathtt{Latt}(A)\to\mathcal{Q}(S+U)$ such that

[TABLE]

We set $\chi^{\prime}(\pi)=f^{\prime}$, where $f^{\prime}:\mathtt{Latt}(A)\to\mathcal{Q}(S)$ is defined by $\theta\mapsto f(\theta)\cap S$ for each $\theta\in\mathtt{Latt}(A)$. This move is legal since $v\in S$ and by naturality of $\lambda$. It is easy to see how to extend the shadow match for each response by $\forall$.

If the last position on the shadow match is $(\underline{\Box}\psi,v)$ then since this position is winning for $\exists$, it must be the case that every position $(\psi,w)$ for $w\in S+U$ is winning for $\exists$, hence this holds for every $w\in U$. This can only be true if $\psi$ is $\mathbb{A}$-valid and so we have $t(\underline{\Box}\psi)=\top$. This means we are done since $(\top,v)$ is a winning position for $\exists$. Similarly, if the last position on the shadow match is $(\underline{\Diamond}\psi,v)$, then there is some $w\in S+U$ such that $(\psi,w)$ is winning for $\exists$, so $\psi$ is $\mathbb{A}$-satisfiable. Hence $t(\underline{\Diamond}\psi)=\top$, and the conclusion follows as in the previous case.

We can now prove our characterization theorem:

Theorem 47**.**

Let $\mathsf{T}$ be any set functor and let $\Lambda$ be any set of predicate liftings for $\mathsf{T}$. Then:

[TABLE]

Proof 6.3**.**

Suppose a formula $\varphi$ of $\mu\mathtt{ML}_{\Lambda\cup\{\underline{\Box}\}}$ is invariant for $\mathsf{T}$-bisimilation. By the finite model property for $\mu\mathtt{ML}_{\Lambda\cup\{\underline{\Box}\}}$ it suffices to show that $\varphi$ is equivalent to a $\mu\mathtt{ML}_{\Lambda}$-formula over finite models. Let $\mathbb{A}$ be a modal $\Lambda\cup\{\underline{\Box}\}$-automaton equivalent to $\varphi$, and let $\psi$ be a formula of $\mu\mathtt{ML}_{\Lambda}$ equivalent to the automaton $t(\mathbb{A})$. Consider an arbitrary finite pointed $\underline{\mathsf{T}}$-model $(\mathbb{S},s)$. We have:

[TABLE]

as required.

6.2. An adequate uniform construction for $\underline{\mathcal{M}}$

In this section we shall apply Corollary 35 to derive a characterization result for the monotone $\mu$-calculus. The first fact that we need is the following:

Proposition 48**.**

The set of liftings $\{\Box,\underline{\Box}\}$ is expressively complete with respect to $\underline{\mathcal{M}}$.

Proof 6.4**.**

Since $\underline{\mathcal{M}}$ preserves weak pullbacks, it suffices by Proposition 14 to show that the one-step language $\mathtt{1ML}_{\{\Box,\underline{\Box}\}}$ has the same expressive power as the language based on the Moss liftings for $\underline{\mathcal{M}}$. Given a finite set $A$, a subset $\Gamma\subseteq\mathtt{Latt}(A)$ and some $N\in\mathcal{M}\mathtt{Latt}(A)$ that is supported by $\Gamma$, we want to define a formula $\gamma$ in $\mathtt{1ML}_{\{\Box,\underline{\Box}\}}$ such that

[TABLE]

This formula can be obtained as a conjunction $\theta_{\Gamma}\wedge\theta_{N}$, where $\theta_{\Gamma}$ is like the standard nabla-formula for the powerset functor corresponding to $\Gamma$, but expressed in terms of the support modality, and $\theta_{N}$ is defined as the nabla formulas for the monotone neighborhood functor introduced by Santocanale and Venema in [30]. We omit the details.

The remainder of this section is devoted to defining a uniform construction for the supported companion $\underline{\mathcal{M}}$ of $\mathcal{M}$ w.r.t. a given finite set of formulas, and prove its adequacy. We proceed as follows: throughout the section we fix an arbitrary natural number $k$ and a finite set of variables $A$, and define a uniform construction $(-)_{*}$ which will be shown to be adequate for every formula in $\mathtt{1SO}_{\{\Box,\underline{\Box}\}}(A)$ of quantifier depth $\leq k$. It clearly follows that there is an adequate uniform construction for every finite set $\Gamma$ of formulas in $\mathtt{1SO}_{\{\Box,\underline{\Box}\}}$, since we can apply the result to the maximum quantifier depth of any formula in $\Gamma$.

To simplify notation a bit, we note that it suffices to define our uniform construction for what we may call normal one-step $\underline{\mathcal{M}}$-frames $(X,(S,\alpha))$, satisfying the condition that $S=X$, and prove that the adequacy condition holds for all models based on such frames. It is then a straightforward matter to extend this to an adequate uniform construction defined on all $\underline{\mathcal{M}}$-frames. We shall denote a normal one-step frame $(X,(X,\alpha))$ more simply by just $(X,\alpha)$. Then for any two normal $\underline{\mathcal{M}}$-models $(X,\alpha,V)$ and $(X^{\prime},\alpha^{\prime},V^{\prime})$ over $A$, i.e. models that are based on normal one-step frames, a relation $R\subseteq X\times X^{\prime}$ is a one-step $\overline{(\underline{\mathcal{M}})}$-bisimulation between these models if, and only if:

• •

$uRu^{\prime}$ implies $u\in V(a)$ iff $u^{\prime}\in V^{\prime}(a)$, for all $a\in A$;

• •

for all $Z$ in $\alpha$ there is $Z^{\prime}$ in $\alpha^{\prime}$ such that for all $t^{\prime}\in Z^{\prime}$ there is $t\in Z$ with $tRt^{\prime}$;

• •

for all $Z^{\prime}$ in $\alpha^{\prime}$ there is $Z$ in $\alpha$ such that for all $t\in Z$ there is $t^{\prime}\in Z^{\prime}$ with $tRt^{\prime}$;

• •

for all $u\in X$ there is $u^{\prime}\in X^{\prime}$ with $uRu^{\prime}$;

• •

for all $u^{\prime}\in X^{\prime}$ there is $u\in X$ with $uRu^{\prime}$.

The last two conditions just say that the relation $R$ is full on $X$ and $X^{\prime}$. We call such a relation a global neighborhood bisimulation between $(X,\alpha,V)$ and $(X^{\prime},\alpha^{\prime},V^{\prime})$. For any normal one-step frame $(X,\alpha)$, we shall construct a cover $h_{\alpha}:(X_{*},\alpha_{*})\to(X,\alpha)$ where $(X_{*},\alpha_{*})$ is also a normal one-step frame. Since these are abbreviated notations for the one-step $\underline{\mathcal{M}}$-frames $(X,(X,\alpha))$ and $(X_{*},(X_{*},\alpha_{*}))$, we should have $\underline{\mathcal{M}}h_{\alpha}(X_{*},\alpha_{*})=(X,\alpha)$, which means that $h_{\alpha}$ should be a surjective map from $X_{*}$ to $X$, such that $\mathcal{M}h_{\alpha}(\alpha_{*})=\alpha$. The intuition behind the construction is that we want to create infinitely many disjoint copies of each neighborhood, and furthermore we want to create sufficiently many copies of each state within each copy of a neighborhood. {defi}

Given a set $X$, and an object $\alpha\in\mathcal{M}X$, put

[TABLE]

and let $\pi_{X}$ be the projection map from $X_{*}$ to $X$. Define $\alpha_{*}\in\mathcal{M}(X_{*})$ by setting $Z\in\alpha_{*}$ for $Z\subseteq X_{*}$ iff $\left\lceil Y,j\right\rceil\subseteq Z$ for some $Y\in\alpha$ and some $j<\omega$, where

[TABLE]

The sets of the form $\left\lceil Y,j\right\rceil$ for $Y\in\alpha$ will be called the basic members of $\alpha_{*}$. The set of all elements in $X_{*}$ that do not belong to any basic member will be called the residue of the frame $(X_{*},\alpha_{*})$. Note that $X_{*}$ is partitioned into each of the basic members along with the residue, as an extra partition cell.

Proposition 49**.**

For every given normal one-step frame $(X,\alpha)$, the projection map $\pi_{X}:(X_{*},\alpha_{*})\to(X,\alpha)$ is a cover.

Proof 6.5**.**

Clearly the projection map $\pi_{X}$ is always surjective since $(u,0,\emptyset,0)\mapsto u$ for all $u\in X$. (Note that $0<2^{n}$ for all $n\in\omega$, so we always have $(u,0,\emptyset,0)\in X_{*}$.)

We need to check that $\mathcal{M}\pi_{X}(\alpha_{*})=\alpha$. In other words, we have to check that for all $Z\subseteq X$, we have $Z\in\alpha$ iff $\pi_{X}^{-1}(Z)\in\alpha_{*}$. For left to right, if $Z\in\alpha$ then $\left\lceil Z,0\right\rceil$ is a basic member of $\alpha_{*}$, and clearly $\left\lceil Z,0\right\rceil\subseteq\pi_{X}^{-1}(Z)$. Conversely, suppose $\pi_{X}^{-1}(Z)\in\alpha_{*}$. Then there is some basic member $\left\lceil Y,j\right\rceil\in\alpha_{*}$ with $\left\lceil Y,j\right\rceil\subseteq\pi_{X}^{-1}(Z)$. But then $Y\in\alpha$, and furthermore $Y\subseteq Z$: if $u\in Y$ then $(u,0,Y,j)\in\left\lceil Y,j\right\rceil$, so $(u,0,Y,j)\in\pi_{X}^{-1}(Z)$ meaning that $\pi_{X}(u,0,Y,j)=u\in Z$. So $Z\in\alpha$ as required.

Our goal is to show that, for any pair of normal and globally neighborhood bisimilar models $(X,\alpha,V)$ and $(Y,\beta,U)$, the corresponding models $(X_{*},\alpha_{*},V_{[\pi_{X}]})$ and $(Y_{*},\beta_{*},U_{[\pi_{Y}]})$ satisfy the same formulas in $\mathtt{1SO}_{\{\Box,\underline{\Box}\}}(A)$ of quantifier depth $\leq k$. It should not be too surprising that we can prove this, but the actual proof is not entirely trivial. It suffices to check it for formulas in which the operator $\underline{\Box}$ and $\underline{\Diamond}$ does not occur, since over normal one-step models this operator is easily definable using the second-order quantifiers. From now on we keep the models $(X,\alpha,V)$ and $(Y,\beta,U)$ fixed, as well as a global neighborhood bisimulation $R$ relating these models. Throughout this section, we use the notation $(X,\alpha,V)\equiv_{k}(Y,\beta,U)$ to say that two one-step models satisfy the same formulas of $\mathtt{1SO}_{\{\Box,\underline{\Box}\}}(A)$ with at most $k$ nested quantifiers.

{defi}

A propositional $A$-type $\tau$ is a subset of $A$. Given a set $X$ and a valuation $V:A\rightarrow\mathcal{Q}(X)$, the propositional $A$-type of $v\in X$ is defined to be $V^{\dagger}(v)=\{a\in A\mid v\in V(a)\}$.

Given a subset $Z$ of $X_{*}$ or $Y_{*}$, a valuation $W$ such that $W:B\rightarrow\mathcal{Q}(X_{*})$ or $W:B\rightarrow\mathcal{Q}(Y_{*})$, and a natural number $m$, the $m$-signature of $Z$ over $B$ relative to the valuation $W$ is the mapping $\sigma_{Z}:\mathcal{P}(B)\rightarrow\{0,...,m\}$ defined by:

[TABLE]

{defi}

Let $B$ be any set of variables containing $A$, and let $V_{1}:B\rightarrow\mathcal{Q}(X_{*})$ and $V_{2}:B\rightarrow\mathcal{Q}(Y_{*})$. Then for any natural number $n$ we write

[TABLE]

and say that these one-step models match up to depth $n$, if:

1. (1)

For every $n$-signature $\sigma$ over variables $B$, the number of basic elements of signature $\sigma$ in $\alpha_{*}$ and $\beta_{*}$ respectively are either both finite and equal, or both infinite. 2. (2)

The residues of the two one-step models have the same $n$-signature.

Using the assumption that the models $(X,\alpha,V)$ and $(Y,\beta,U)$ are globally neighborhood bisimilar, we get the following lemma.

Lemma 50**.**

$(X_{*},\alpha_{*},V_{[\pi_{X}]})\approx_{2^{k}}(Y_{*},\beta_{*},U_{[\pi_{Y}]})$.

Proof 6.6**.**

To see that the residues of the two models have the same $2^{k}$-signature, for one direction just note that if the residue of $(X_{*},\alpha_{*},V_{[\pi_{X}]})$ contains an element $(u,i,Z,j)$ then it contains infinitely many elements of the same propositional type, namely one member $(u,i,Z,p)$ for every $p\in\omega$. But then so will the residue of $(Y_{*},\beta_{*},U_{[\pi_{Y}]})$: just pick some $v$ with $uRv$ (again using the fact that $R$ is a global neighborhood bisimulation). Since $v\notin\emptyset$, for every $p\in\omega$ the element $(v,0,\emptyset,p)$ will be a member of the residue of $(Y_{*},\beta_{*},U_{[\pi_{Y}]})$ of the same propositional type as $(u,i,Z,j)$.

Now for the basic elements. First note that, for any $2^{k}$-signature $\sigma$, $\alpha_{*}$ either contains no basic elements of signature $\sigma$, or infinitely many: if there is some basic element $\left\lceil Z,j\right\rceil$ of signature $\sigma$, then for any $i\neq j$, the basic element $\left\lceil Z,i\right\rceil$ has the same $2^{k}$-signature as $\left\lceil Z,j\right\rceil$ with respect to the valuation $V_{[\pi_{X}]}$. The same holds for $\beta_{*}$ with respect to the valuation $U_{[\pi_{Y}]}$. Hence, it suffices to show that $\alpha_{*}$ contains a basic element of signature $\sigma$ w.r.t. $V_{[\pi_{X}]}$ iff $\beta_{*}$ contains a basic element of signature $\sigma$ w.r.t $U_{[\pi_{Y}]}$.

We consider only one direction: suppose that $\alpha_{*}$ contains a basic element $\left\lceil Z,j\right\rceil$ of signature $\sigma$, where $Z\in\alpha$. Then there must be $Z^{\prime}\in\beta$ such that, for all $v\in Z^{\prime}$, there is $u\in Z$ with $uRv$, since $R$ was a global neighborhood bisimulation. Furthermore, since $R$ is full on $X$, for every $w\in Z$ we can pick some $w^{\prime}\in Y$ with $wRw^{\prime}$, and put

[TABLE]

By monotonicity we have $Z^{\prime\prime}\in\beta$. Furthermore, $Z$ and $Z^{\prime\prime}$ are clearly related so that the following back-and-forth conditions hold: for all $u\in Z$ there is $v\in Z^{\prime\prime}$ with $uRv$, and for all $v\in Z^{\prime\prime}$ there is $u\in Z$ with $uRv$. Since any two states related by $R$ have the same propositional type, it follows that the same propositional types appear in $\left\lceil Z,j\right\rceil$ and $\left\lceil Z^{\prime\prime},j\right\rceil$. But since both these sets contain at least $2^{k}$ copies of every propositional type that appears in them, it follows that $\left\lceil Z,j\right\rceil$ and $\left\lceil Z^{\prime\prime},j\right\rceil$ have the same $2^{k}$-signature, as required.

We are going to show, by induction on a natural number $m\leq k$, that if two one-step models of the form $(X_{*},\alpha_{*},V_{1})$ and $(Y_{*},\beta_{*},V_{2})$ match up to depth $2^{m}$, then they satisfy the same formulas of quantifier depth $m$. Together with the previous lemma, it then follows that the one-step models $(X_{*},\alpha_{*},V_{[\pi_{X}]})$ and $(Y_{*},\beta_{*},U_{[\pi_{Y}]})$ satisfy the same formulas of quantifier depth $\leq k$. For the basis case of $2^{0}=1$, we need the following result (we recall that the case of atomic formulas $\underline{\Box}a$ can be safely ignored):

Lemma 51**.**

Let $B$ be a set of variables containing $A$, and let $V_{1}:B\rightarrow\mathcal{Q}(X_{*})$ and $V_{2}:B\rightarrow\mathcal{Q}(Y_{*})$ be valuations such that

[TABLE]

Then these two one-step models satisfy the same atomic formulas of the one-step language $\mathtt{1SO}_{\{\Box\}}(B)$.

Proof 6.7**.**

We only prove one direction for each case.

Suppose first that

[TABLE]

where $p,q\in B$. Suppose for a contradiction that $V_{2}(p)\nsubseteq V_{2}(q)$. Then there is some $(u,i,Z,j)\in Y_{*}$ such that $(u,i,Z,j)\in V_{2}(p)\setminus V_{2}(q)$. If $(u,i,Z,j)$ comes from the residue of $(Y_{*},\beta_{*})$ then since the residue of $(X_{*},V_{*})$ has the same $1$-signature, it must contain some element $(u^{\prime},i^{\prime},Z^{\prime},j^{\prime})$ of the same $1$-type, and so we cannot have $V_{1}(p)\subseteq V_{1}(p)$. The case where $(u,i,Z,j)$ comes from a basic member is similar.

Now, suppose that

[TABLE]

Then $V_{1}(p)\in\alpha_{*}$, so there is some basic element $\left\lceil Z,j\right\rceil\in\alpha_{*}$ with $\left\lceil Z,j\right\rceil\subseteq V_{1}(p)$. There must be some basic $\left\lceil Z^{\prime},j^{\prime}\right\rceil\in\beta_{*}$ of the same $1$-signature over $B$ as $\left\lceil Z,j\right\rceil$, and clearly it follows that $\left\lceil Z^{\prime},j^{\prime}\right\rceil\subseteq V_{2}(p)$ and so $V_{2}(p)\in\beta_{*}$ as required.

We now only need the following lemma:

Lemma 52**.**

Let $B$ be a finite set of variables containing $A$, let $0<m\leq k$ and let $V_{1}:B\rightarrow Q(X_{*})$ and $V_{2}:B\rightarrow\mathcal{Q}(Y_{*})$ be valuations such that

[TABLE]

Let $q$ be any fresh variable. Then for any valuation $V_{1}^{\prime}$ over $B\cup\{q\}$ extending $V_{1}$ with some value for $q$, there exists a valuation $V_{2}^{\prime}$ over $B\cup\{q\}$ extending $V_{2}$, such that

[TABLE]

and vice versa.

Proof 6.8**.**

We only prove one direction since the other direction can be proved by a symmetric argument.

Let $V_{1}^{\prime}$ be given. By the hypothesis, for any $2^{m}$-signature $\sigma$ over the variables $B$, the number of basic elements of signature $\sigma$ in $\alpha_{*}$ and $\beta_{*}$ relative to $V_{1}$ and $V_{2}$ are either both finite and the same, or both infinite. Let $\sigma_{1},...,\sigma_{k}$ be a list of all the distinct $2^{m}$-signatures over $B$ such that the set of basic elements of $\alpha_{*}$ and $\beta_{*}$ of signature $\sigma_{i}$, with $1\leq i\leq k$, is non-empty but finite, and let $\sigma_{k+1},...,\sigma_{l}$ be a list of all the $2^{m}$-signatures such that, for $k+1\leq i\leq l$, there are infinitely many basic elements of $\alpha_{*}$ and of $\beta_{*}$ of signature $\sigma_{i}$. Then, for each $i\in\{1,...,l\}$, let $\alpha_{*}[\sigma_{i}]$ denote the set of basic elements in $\alpha_{*}$ of signature $\sigma_{i}$, and similarly let $\beta_{*}[\sigma_{i}]$ denote the set of basic elements of $\beta_{*}$ of signature $\sigma_{i}$. Then $\alpha_{*}[\sigma_{1}],...,\alpha_{*}[\sigma_{l}]$ is a partition of the set of basic elements of $\alpha_{*}$ into non-empty cells, and similarly $\beta_{*}[\sigma_{1}],...,\beta_{*}[\sigma_{l}]$ is a partition of the set of basic elements of $\beta_{*}$.

Given the extended valuation $V_{1}^{\prime}$ on $X_{*}$ defined on variables $B\cup\{q\}$, we similarly let $\tau_{1},...,\tau_{k^{\prime}}$ be a list of all the $2^{m-1}$-signatures over $B\cup\{q\}$ such that, for $1\leq i\leq k^{\prime}$, the set of basic elements of $\alpha_{*}$ of $2^{m-1}$-signature $\tau_{i}$ is non-empty but finite. We let $\tau_{k^{\prime}+1},...,\tau_{l^{\prime}}$ be a list of all the $2^{m-1}$-signatures over $B\cup\{q\}$ such that, for each $i$ with $k^{\prime}+1\leq i\leq l^{\prime}$, the set of basic elements of $\alpha_{*}$ of $2^{m-1}$-signature $\tau_{i}$ is infinite. Let $\alpha_{*}[\tau_{i}]$ denote the set of basic elements of $\alpha_{*}$ of $2^{m-1}$-signature $\tau_{i}$, so that the collection $\alpha_{*}[\tau_{1}],...,\alpha_{*}[\tau_{l^{\prime}}]$ constitutes a second partition of the set of basic elements of $\alpha_{*}$. It will be useful to introduce the abbreviation $D_{1}$ for the finite set $\alpha_{*}[\sigma_{1}]\cup...\cup\alpha_{*}[\sigma_{k}]$, and the abbreviation $D_{2}$ for the finite set $\alpha_{*}[\tau_{1}]\cup...\cup\alpha_{*}[\tau_{k^{\prime}}]$.

For each $i$ with $1\leq i\leq k$, there is a bijection between the set $\alpha_{*}[\sigma_{i}]$ and $\beta_{*}[\sigma_{i}]$, and we can paste all these bijections together into a bijective map

[TABLE]

Since every basic element of $\alpha_{*}$ not in $D_{1}$ belongs to a $2^{m}$-signature of which there are infinitely many basic elements in $\beta_{*}$, and since $D_{1}\cup D_{2}$ is finite, it is easy to see that we can extend the map $f$ to a map $g$ which is an injection from the set $D_{1}\cup D_{2}$ into the set of basic elements of $\beta_{*}$, such that for each basic element $\left\lceil Z,j\right\rceil$ in $D_{1}\cup D_{2}$, $\left\lceil Z,j\right\rceil$ and $g(\left\lceil Z,j\right\rceil)$ have the same $2^{m}$-signature over $B$, and such that $g\!\upharpoonright\!D_{1}=f$. Each basic element of $\beta_{*}$ not in the image of $g$ must then be of one of the $2^{m}$-signatures $\sigma_{k+1},...,\sigma_{l}$, and so we can partition the set of basic elements of $\beta_{*}$ outside the image of $g$ into the cells $\beta_{*}[\sigma_{k+1}]\setminus g[D_{2}],...,\beta_{*}[\sigma_{l}]\setminus g[D_{2}]$. For each $i$ with $k+1\leq i\leq l$, let $\gamma^{i}_{1},...,\gamma^{i}_{r}$ list all infinite sets of the form $\alpha_{*}[\sigma_{i}]\cap\alpha_{*}[\tau_{j}]$ for $k^{\prime}+1\leq j\leq l^{\prime}$. The list $\gamma^{i}_{1},...,\gamma^{i}_{r}$ must be non-empty, and so since the set $\beta_{*}[\sigma_{i}]\setminus g[D_{2}]$ is also infinite, we may partition it into $r$ many infinite cells and list these as $\delta^{i}_{1},...,\delta^{i}_{r}$. Now, for each basic element $\left\lceil Z,j\right\rceil$ of $\beta_{*}$, we define a map $W_{\left\lceil Z,j\right\rceil}$ from $B\cup\{q\}$ to $\mathcal{P}(\left\lceil Z,j\right\rceil)$ by a case distinction as follows:

Case 1:* $\left\lceil Z,j\right\rceil=g(\left\lceil Z^{\prime},j^{\prime}\right\rceil)$ for some $\left\lceil Z^{\prime},j^{\prime}\right\rceil\in D_{1}\cup D_{2}$. Then $\left\lceil Z,j\right\rceil$ and $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ have the same $2^{m}$-signature over $B$. Using this fact we define the valuation $W_{\left\lceil Z,j\right\rceil}$ so that, for each $p\in B$, we have $W_{\left\lceil Z,j\right\rceil}(p)=V_{2}(p)\cap\left\lceil Z,j\right\rceil$, and so that $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ and $\left\lceil Z,j\right\rceil$ have the same $2^{m-1}$-signature over $B\cup\{q\}$ with respect to the valuations $V_{1}^{\prime}$ and $W_{\left\lceil Z,j\right\rceil}$. We show how to assign the value of the variable $q$: for each propositional type $t$ over $B\cup\{q\}$, there are three different possible cases to consider. If $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ has $m^{\prime}<2^{m-1}$ elements of type $t\cup\{q\}$ over $B\cup\{q\}$, then pick $m^{\prime}$ many elements of $\left\lceil Z,j\right\rceil$ of type $t$ and mark them by $q$. This is possible since $m^{\prime}<2^{m-1}\leq 2^{m}$ and $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ and $\left\lceil Z,j\right\rceil$ have the same $2^{m}$-signature. If there are $m^{\prime}<2^{m-1}$ elements of $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ of type $t$ over $B\cup\{q\}$, then pick $m^{\prime}$ elements of $\left\lceil Z,j\right\rceil$ of type $t$ over $B$, and mark all the other elements of $\left\lceil Z,j\right\rceil$ of type $t$ by $q$. Finally, if there are at least $2^{m-1}$ elements of $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ of type $t\cup\{q\}$ over $B\cup\{q\}$ and at least $2^{m-1}$ elements of $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ of type $t$ over $B\cup\{q\}$, then all in all there must be at least $2^{m}$ elements of $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ of type $t$ over $B$, and so there must be at least $2^{m}$ elements of $\left\lceil Z,j\right\rceil$ of type $t$ over $B$. Pick $2^{m-1}$ of these and mark them by $q$. Finally, let $W_{\left\lceil Z,j\right\rceil}(q)$ be the set of elements of $\left\lceil Z,j\right\rceil$ marked by $q$.*

Case 2:* $\left\lceil Z,j\right\rceil$ is not in the image of $g$. Then there must be some $i\in\{k^{\prime}+1,...,l^{\prime}\}$ such that $\left\lceil Z,j\right\rceil\in\beta_{*}[\sigma_{k+1}]\setminus g[D_{2}]$, and this set is partitioned into $\delta^{i}_{1},...,\delta^{i}_{r}$. Let $\left\lceil Z,j\right\rceil\in\delta^{i}_{j}$, and pick some arbitary element $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ of the set $\gamma^{i}_{j}$. Then $\left\lceil Z^{\prime},j^{\prime}\right\rceil$ and $\left\lceil Z,j\right\rceil$ have the same $2^{m}$-signature over $B$ and we can proceed as in Case 1.*

We define the valuation $V_{2}^{\prime}$ so that the intersection of $V_{2}^{\prime}(q)$ with the union of all the basic members of $\beta_{*}$ equals the union of the sets $W_{\left\lceil Z,j\right\rceil}(q)$ for $\left\lceil Z,j\right\rceil$ a basic element in $\beta_{*}$, and so that the residue of $(Y_{*},\beta_{*})$ has the same $2^{(m-1)}$-signature as the residue of $(X_{*},\alpha_{*})$ with respect to the valuations $V_{1}^{\prime}$ and $V_{2}^{\prime}$. This can be done using the same reasoning as in the two previous cases. We now need to check that

[TABLE]

First, suppose there are infinitely many basic elements of $\alpha_{*}$ of some $2^{m-1}$ signature $\tau_{j}$, meaning that $k^{\prime}\leq j\leq l^{\prime}$. Then since the set $\alpha_{*}[\tau_{j}]$ is infinite, $D_{1}$ is finite and

[TABLE]

there must be some $i\in\{k+1,...,l\}$ such that the set $\alpha_{*}[\sigma_{i}]\cap\alpha_{*}[\tau_{j}]$ is infinite. This means that $\alpha_{*}[\sigma_{i}]\cap\alpha_{*}[\tau_{j}]$ appears in the list $\gamma^{i}_{1},...,\gamma^{i}_{r}$, and so we see that all elements of some member of the list $\delta^{i}_{1},...,\delta^{i}_{r}$ will have the $2^{m-1}$-signature $\tau_{j}$. Since each member of this list is infinite, we see that there must be infinitely many basic elements of $\beta_{*}$ of signature $\tau_{j}$.

Conversely, suppose there are infinitely many basic elements of $\beta_{*}$ of $2^{m-1}$-signature $\tau_{j}$ over $B\cup\{q\}$. Then since the image of $g$ is finite, some of these elements must be outside the image of $g$, which means that for some $i\in\{k+1,...,l\}$, some member of the list $\delta^{i}_{1},...,\delta^{i}_{r}$ will consist of elements of signature $\tau_{j}$. This means that some member of the list $\gamma_{1}^{i},...,\gamma_{r}^{i}$ will consist of elements of signature $\tau_{j}$, and since each member of this list is infinite we see that $\alpha_{*}$ has infinitely many basic elements of $2^{m-1}$-signature $\tau_{j}$ over $B\cup\{q\}$.

Finally, suppose that there are finitely many basic elements of $\alpha_{*}$ and $\beta_{*}$ of $2^{m-1}$-signature $\tau_{j}$. We check that the mapping $g$ restricts to a bijection between the basic elements of $\alpha_{*}$ and $\beta_{*}$ of this signature. First, $g$ is injective and maps basic elements of $\alpha_{*}$ of signature $\tau_{j}$ to basic elements of $\beta_{*}$ of signature $\tau_{j}$. It only remains to show that (the restriction of) $g$ is surjective, i.e. each basic element $\left\lceil Z,r\right\rceil$ of signature $\tau_{j}$ is equal to $g(\left\lceil Z^{\prime},r^{\prime}\right\rceil)$ for some $\left\lceil Z^{\prime},r^{\prime}\right\rceil$. But suppose $\left\lceil Z,r\right\rceil$ is not in the image of $g$; then it is in one of the members of the list $\delta_{1}^{i},...,\delta_{r}^{i}$ for some $i$, and since each of these members is an infinite set of basic elements of the same signature, we see that there are infinitely many basic elements of $\beta_{*}$ of signature $\tau_{j}$, contrary to our assumption. Hence, the proof is done.

Theorem 53**.**

The monotone $\mu$-calculus is the neighborhood bisimulation invariant fragment of monotone monadic second-order logic. In a formula:

[TABLE]

Proof 6.9**.**

It suffices to prove that $\mathtt{MSO}_{\{\Box,\underline{\Box}\}}{/}{\sim}$ is equal to $\mu\mathtt{ML}_{\{\Box,\underline{\Box}\}}$, and then apply Theorem 47. For this, by Theorem 2 it suffices in turn to prove that the construction $(-)_{*}$ is adequate for all formulas in $\mathtt{1SO}_{\{\Box,\underline{\Box}\}}(A)$ of quantifier depth $\leq k$. We can prove this by combining the last three lemmas, using Ehrenfeucht-Fraïssé games for the one-step language. Lemmas 50 and 52 provide a recipe for how “Duplicator” can survive $k$ steps of the game comparing the models $(X_{*},\alpha_{*},V_{[\pi_{X}]})$ and $(Y_{*},\beta_{*},U_{[\pi_{Y}]})$, and 51 guarantees that the valuations constructed at the end of the game will satisfy the same atomic formulas. Working out the full argument is entirely standard, so we leave the details to the reader.

7. Future work

We conclude by mentioning some questions for future research:

1. (1)

Is there a good categorical and “logic free” characterization of those set functors $\mathsf{T}$ that admit an adequate (or weakly adequate) uniform construction, for instance, in terms of $\mathsf{T}$ preserving certain limits or colimits? Trying to answer this question would involve a deeper study of how the model theory of one-step languages is related to categorical properties of the type functor involved. Related to this, an anonymous referee pointed out to us that the machinery of one-step frames, covers and uniform constructions are all taking place in the category of elements associated with the set functor $\mathsf{T}$, and properties of the functor $\mathsf{T}$ are closely related to properties of the corresponding category of elements [2]. This could very well be a fruitful direction to investigate further. 2. (2)

Can we improve our work on the supported companion functor, to the effect that every set functor $\mathsf{T}$ has a companion $\mathsf{T}^{\prime}$ that admits an adequate uniform construction? Relating this to the previous question, we would like to understand why the supported companion to $\mathcal{M}$ admits an adequate uniform construction, but not $\mathcal{M}$ itself. The construction achieves two things, in general: first, it ensures that every $\alpha\in\underline{\mathsf{T}}X$ has a unique smallest support (even when $X$ is infinite), often called its base. Second, and in our view more importantly, we get that the map $\mathsf{base}_{X}:\underline{\mathsf{T}}X\to\mathcal{P}X$ defined by sending each $\alpha$ to its base is a natural transformation. Conditions for a functor under which this holds has been isolated by Gumm in [9]. Are these conditions related to the existence of adequate uniform constructions? 3. (3)

It would be interesting to further explore the relation between $\mathtt{MSO}_{\mathsf{T}}$ and the first-order logic of Litak & alii [17] for $\mathsf{T}$-coalgebras. For instance, an interesting question would be whether (on $\mathsf{T}$-tree models) $\mathtt{MSO}_{\mathsf{T}}$ is equivalent to some extension of this first-order language with fixpoint operators. 4. (4)

Finally, there is the question of finding sufficient and necessary conditions for a Janin-Walukiewicz theorem to hold. Related to this question, we have not been able to produce an example of a functor for which the Janin-Walukiewicz theorem does not hold (the question of whether such an example can be found was raised to us by an anonymous referee). Given all that we can say for sure, it could be the case that a Janin-Walukiewicz theorem simply holds for every set functor, but we conjecture that at least some conditions on the functor are required.

Acknowledgement

We wish to thank the anonymous referees for their very thorough and constructive feedback, which led to many substantial improvements on the original draft of this paper.