Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This note is not a survey of coalgebraic logics such as [1, 2]. Instead, I am going to highlight ideas that continue to be important for my research within the area. A leitmotif is the fundamental role played by duality theory.

1 Logics for Coalgebras

The concepts behaviour and observation are central for the coalgebraic modelling of systems. Whereas behaviour is formalised within the theory of Universal Coalgebra [3] via bisimilarity and finality, it is less clear how to devise a matching notion of observations that allows to formally specify, verify and reason about this behaviour. Providing such a theory of observations is an important goal that has been driving the development of coalgebraic logics.

Why Modal Logic? A simple answer to this question is that basic modal logic is the logic of Kripke frames and Kripke frames are coalgebras for the covariant power set functor \(\mathcal {P}\). More importantly, modal logics usually express properties that are invariant under bisimulations which matches our intuition that formulas of a coalgebraic logic should allow to observe coalgebraic behaviour. In addition to that, a more categorical answer was provided in [4,5,6] where it was shown that the abstract relationship between coalgebra and modal logic dualises the fundamental link between algebra and equational logic. A basic problem that had to be overcome was to devise suitable (and usable!) modal languages that would allow to specify properties about coalgebras. Probably the two most successful proposals where on the one hand Moss’ \(\nabla \)-modality [7, 8] (which originally was denoted by \(\varDelta \)) that made the radical step to use the coalgebraic type functor as a syntax constructor of the logic and, on the other hand, Pattinson’s logic given by predicate liftings [9]. Another important line of research was to use the syntactic structure of polynomial functors to inductively define corresponding modal operators [10,11,12]. This research helped to develop one of the key features of coalgebraic modal logics: languages and deduction systems can be composed in an elegant, seamless fashion [13, 14] that mirrors the composition of functors.

Expressive Languages. One criterion for what a suitable language for specifying coalgebra is, is the so-called Hennessy-Milner property stating that two coalgebra states are bisimilar iff they satisfy the same formulas of the language. A language that satisfies this property is often called expressive. It is clear that expressive languages do not exist for functors for which there is no final coalgebra [15,16,17]. An important positive result in coalgebraic modal logic states that for finitary set functors there is a always an expressive language of predicate liftings [18]. Its proof uses an alternative characterisation of predicate liftings via the Yoneda Lemma. Similarly, for finitary, weak pullback preserving set functors, the \(\nabla \)-language is always expressive, a statement that is easily proven using terminal sequence induction. Other positive results include functors on the category of Stone spaces [19] and measure spaces [20]. In these cases the proof of expressivity goes via a logical construction of final coalgebras that proves expressivity of the language at the same time as completeness of the logic.

Logics via a Dual Adjunction. All modal languages for coalgebras can be abstractly described via a dual adjunction

(1)

together with a natural transformation \(\delta : L \circ F \rightarrow F \circ T\), sometimes referred to as the “one-step semantics” of the language. One of the first papers advocating this view was probably [21] but only for the restricted case of the well-known dual equivalence between the category of Stone Spaces and the category of Boolean algebras whereas the more general picture above was fully developed in [22]. The abstract approach allows on the one hand to formulate properties of the logic as properties of \(\delta \), eg., completeness of the logic is linked to \(\delta \) being componentwise mono whereas expressivity to its mate \(\delta ^\sharp : T \circ G \rightarrow G \circ L\) having that property (cf. [22, 23]). Since then several researchers have pushed this approach significantly further covering - for example - positive modal logics [24], process algebra [25] and logics for trace equivalence [26], to name just a few.

2 The Power Law for \(\nabla \)

A Distributive Law For \(\varvec{\nabla }\). While the duality-based approach to coalgebraic logics originated for logics based on predicate liftings, it is not too difficult to see that Moss’ original \(\nabla \)-logic also fits into the framework [2]. Key for showing this is the following distributive law

$$\begin{aligned} \rho _\nabla : T \circ \mathcal {P}\rightarrow & {} \mathcal {P}\circ T \\ \pi\mapsto & {} \{ t \in T X \mid (t,\pi ) \in \overline{T}(\in ) \} \end{aligned}$$

that exists for all weak pullback preserving set functors T (the law has been called the power law in [27]). Here \(\overline{T}\) denotes the unique extension of the set functor T to a relator [28]. The significance of this law, however, goes far beyond being the one-step semantics of the \(\nabla \)-logic. It forms the basis of the definition of so-called redistributions [29, 30]. Roughly speaking, an element \(\varXi \in T \mathcal {P}X\) is called redistribution of some \(\varPi \in \mathcal {P}T X\) if \(\varPi \subseteq \rho _{\nabla } (\varXi )\). Redistributions allow to formulate an important logical distributive law for the \(\nabla \)-logic

$$\begin{aligned} \bigwedge _{\pi \in \varPi } \nabla \pi \leftrightarrow \bigvee _{\varXi \in \mathrm {SRD}(\varPi )} \nabla (T \wedge )(\varXi ) . \end{aligned}$$
(2)

where \(\mathrm {SRD}(\varPi )\) the collection of all (slim) redistributions of \(\varPi \). The law is the key for the work [30, 31] developing a complete deduction system for the \(\nabla \)-logic that is entirely parametric in the set functor T.

Coalgebraic Fixpoint Logics. The coalgebraic logics that I have discussed so far can only formulate the finite-step behaviour of a coalgebra. For properties such as liveness (“something will happen infinitely often in the future”) and safety (“at no point in the future the systems will crash”) we need to be able to specify the ongoing, possibly infinite behaviour. A coalgebraic treatment of fixpoint-logics is difficult as duality-based techniques cannot be applied easily [32]. This makes completeness proofs for such logics notoriously hard. Nevertheless these logics have been studied successfully on a coalgebraic level. In the first instance, the focus was on automata for coalgebraic fixpoint logics that employed the \(\nabla \)-operator [33]. The above logical distributive law (2) provided the key to prove important closure properties [29] of these “coalgebra automata” and thus a general finite model property and decidability result. After these initial proof-of-concept results attention shifted to fixpoint logics using predicate liftings. Both automata [34] and tableau-systems [35] were developed - the role of the power law and of redistributions is played by the assumption that the given predicate liftings come with a sound and complete axiomatisation via so-called one-step rules [36]. Apart from these results on checking satisfiability of coalgebraic fixpoint logic research on complete axiomatisations also made gradual progress, first for so-called flat coalgebraic fixpoint logics [37, 38], later for coalgebraic dynamic logics [39] and finally with a recent breakthrough result on completeness for the full coalgebraic \(\mu \)-calculus [40].

3 Current Research

I am now going to list research directions within coalgebraic logic that I am currently focusing on and that I am planning to discuss in my talk.

Coalgebra Automata and Duality. Coalgebra automata play an important role for studying the coalgebraic \(\mu \)-calculus: not only do they provide a tool for deciding satisfiability but they are also instrumental in completeness proofs, cf. e.g. [40]. Building on our recent work for game logic [41] we are working on devising automata for coalgebraic dynamic logics. Furthermore we plan to develop automata that operate on coalgebras over Stone Spaces. A first step in this direction was made in [42] where we obtained a characterisation of the clopen semantics of the (standard) \(\mu \)-calculus in terms of parity games. The long term goal is a completeness proof for coalgebraic fixpoint logics via a duality theoretic argument.

Learning and Duality. In recent work [43] we devised a generalisation of Angluin’s well-known \(L^*\)-algorithm for learning regular languages [44]. The generalisation can be summarised in the following (informally stated) theorem that holds for any finitary set functor \(T\).

Theorem 1

Let \((\mathbb {X},x)\) be a pointed \(T\)-coalgebra that is behaviourally equivalent to a finite well-pointed (=minimal & reachable) \(T\)-coalgebra \((\mathbb {Y},y)\). Let \(\mathcal {L}\) be an expressive language for \(T\)-coalgebras. Our algorithm determines the well-pointed coalgebra \((\mathbb {Y},y)\) using queries and counter-examples from \(\mathcal {L}\).

A key observation that led to the algorithm is that Angluin’s algorithm essentially learns modal filtrations. These filtrations can be defined relative to any coalgebraic logic. In my talk I will discuss the above theorem and report on ongoing work on fitting filtrations and thus learning into the dual adjunction framework of coalgebraic logic.

Possible Application: Iterated Games. In our recent paper [45] we use the framework of open games [46] to represent an infinitely iterated strategic game (such as the well-known Prisoner’s Dilemma) as a final coalgebra. As a byproduct, this work allows to characterise subgame perfect equilibiria using the (standard) coalgebraic \(\mu \)-calculus. To give the reader a rough idea, let me spell out some of the details. Consider a simple game (think of the Prisoner’s Dilemma) with set of moves Y where an element of Y represents the moves played by all players simultaneously. A play of the infinitely iterated game is an infinite sequence of moves \(\rho \in Y^\omega \), strategies in this game are pointed coalgebras of the form

$$\begin{aligned} \langle \mathrm {now}, \mathrm {ltr}\rangle : X \rightarrow Y \times X^Y \end{aligned}$$

where at each state \(x \in X\) the coalgebra map determines the next move \(\mathrm {now}(x)\) and moves to the next state \(\mathrm {ltr}(x)(y')\) depending on which move \(y' \in Y\) has been actually carried out in one round of the game. Pay-off functions for the infinitely iterated game are of type \(k:Y^\omega \rightarrow R\) (where R is typically of the form \(\mathbb {R}^n\) for an n-player game). This leads us to define a coalgebra

$$\begin{aligned} \langle \overline{\mathrm {now}}, \overline{\mathrm {ltr}} \rangle : (X \times R^{Y^\omega }) \longrightarrow Y \times (X \times R^{Y^\omega })^Y \end{aligned}$$

by putting

where \(k_y (\rho ) \mathrel {:=} k(y\rho )\) for \(y \in Y\), \(\rho \in Y^\omega \). The intuition behind this definition is to record the current strategy of the players and the payoff function - both based on the history of the game played thus far. With these definitions in place it is not difficult to see that subgame perfect equilibria in the infinitely repeated game can be characterised via a \(\mu \)-calculus formula \( \psi = \nu X. P \wedge \Box X\) for a suitable predicate P that is defined using the equilibrium of the stage game. The obtained characterisation has the following form:

$$\begin{aligned} (x,k) \models \psi \quad \text{ iff } x \text{ represents } \text{ an } \text{ s.p.equilibrium } \text{ of } \text{ the } \text{ game } \text{ with } \text{ payoff } k . \end{aligned}$$

While the coalgebra \(\langle \overline{\mathrm {now}},\overline{\mathrm {ltr}} \rangle \) will in general be infinite, assumptions on the pay-off function (such as discounted sum) will allow us to obtain a finite equivalent coalgebra. In my talk I will provide the details of this construction and I will explain how this observation connects the afore mentioned automata and learning techniques to game theory.