# Coalgebraic Logics & Duality

Clemens Kupke

► To cite this version:

Clemens Kupke. Coalgebraic Logics & Duality. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.6-12, 10.1007/978-3-030-00389-0_2. hal-02044643

HAL Id: hal-02044643

https://inria.hal.science/hal-02044643

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Coalgebraic Logics & Duality

Clemens Kupke

Department of Computer & Information Sciences
University of Strathclyde
Glasgow, Scotland
clemens.kupke@strath.ac.uk

**Abstract.** I will provide a brief introduction to coalgebraic modal logics and highlight a few central concepts concerning these logics. After that I will outline my current research in the area.

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–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 $\Delta$) 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–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–17]. An important positive result in coalgebraic modal logic states that for finitary set functors there is 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 ∇-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

$$ T \underset{G}{\stackrel{T}{\rightleftharpoons}} C \underset{F}{\stackrel{\perp}{\rightleftharpoons}} \mathcal{D}^{\text{op}} \underset{L}{\stackrel{\leftleftharpoons}{\rightleftharpoons}} L \quad (1) $$

together with a natural transformation $\delta : L \circ F \to 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^\# : T \circ G \to G \circ L$ having that property (cf. [23, 22]). 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 ∇

**A distributive law for ∇** 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 ∇-logic also fits into the framework [2]. Key for showing this is the following distributive law

$$ \rho_{\nabla} : T \circ \mathcal{P} \to \mathcal{P} \circ T \\ \pi \mapsto \{t \in TX \mid (t, \pi) \in \bar{T}(\in)\} $$

that exists for all weak pullback preserving set functors $T$ (the law has been called the *power law* in [27]). Here $\bar{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 ∇-logic. It forms the basis of the definition of so-called redistributions [29, 30]. Roughly speaking, an element Ξ ∈ T P X is called redistribution of some Π ∈ P T X if Π ⊆ ρ$_{∇}$ (Ξ). Redistributions allow to formulate an important logical distributive law for the ∇-logic

$$ \bigwedge_{\pi \in \Pi} \nabla \pi \leftrightarrow \bigvee_{\Xi \in \text{SRD}(\Pi)} \nabla (T \wedge) (\Xi). \qquad (2) $$

where SRD(Π) the collection of all (slim) redistributions of Π. The law is the key for the work [30, 31] developing a complete deduction system for the ∇-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 ∇-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 μ-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 μ-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 equilibria 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

$$ \langle \text{now}, \text{ltr} \rangle : X \to Y \times X^Y $$

where at each state $x \in X$ the coalgebra map determines the next move now($x$) and moves to the next state 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 \to R$ (where $R$ is typically of the form $\mathbb{R}^n$ for an $n$-player game). This leads us to define a coalgebra

$$ \langle \overline{\text{now}}, \overline{\text{ltr}} \rangle : (X \times R^{Y^\omega}) \to Y \times (X \times R^{Y^\omega})^Y $$

by putting

$$ \overline{\text{now}}(x, k) := \text{now}(x) $$

$$ \overline{\text{ltr}}(x, k) := \lambda y. \langle \text{ltr}(x)(y), k_y \rangle $$

where $k_y(\rho) := 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 μ-calculus formula ψ = νX.P ∧ □X for a suitable
predicate P that is defined using the equilibrium of the stage game. The obtained
characterisation has the following form:

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

While the coalgebra $\langle \overline{\text{now}}, \overline{\text{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.

**Acknowledgements** The overview of current research is based on joint work with Simone Barlocco, Nick Bezhanisvili, Neil Ghani, Helle Hvid Hansen, Alasdair Lambert, Johannes Marti, Fredrik Nordvall Forsberg, Jurriaan Rot and Yde Venema.

References

1. Cirstea, C., Kurz, A., Pattinson, D., Schröder, L., Venema, Y.: Modal logics are coalgebraic. The Computer Journal **54** (2011) 31–41

2. Kupke, C., Pattinson, D.: Coalgebraic semantics of modal logics: An overview. TCS **412**(38) (2011) 5070–5094

3. Rutten, J.: Universal coalgebra: A theory of systems. Theoretical Computer Science **249** (2000) 3–80

4. Gumm, H.P., Schröder, T.: Covarieties and complete covarieties. Theor. Comput. Sci. **260**(1-2) (2001) 71–86

5. Kurz, A.: A Co-Variety-Theorem for Modal Logic. In: Advances in Modal Logic 2, CSLI (2001) Selected Papers from AiML 2, Uppsala, 1998.

6. Kurz, A.: Logics for Coalgebras and Applications to Computer Science. PhD thesis, Ludwig-Maximilians-Universität (2000)

7. Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Logic **96**(1-3) (1999) 277–317

8. Moss, L.S.: Erratum to "coalgebraic logic": Ann. pure appl. logic 96 (1999) 277-317.
Ann. Pure Appl. Logic **99**(1-3) (1999) 241-259

9. Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. **309**(1-3) (2003) 177–193

10. Jacobs, B.: Many-sorted coalgebraic modal logic: a model-theoretic study. ITA **35**(1) (2001) 31–59

11. Rößiger, M.: Coalgebras and modal logic. Electr. Notes Theor. Comput. Sci. **33** (2000) 294–315

12. Goldblatt, R.: Equational logic of polynomial coalgebras. In Balbiani, P., Suzuki, N., Wolter, F., Zakharyaschev, M., eds.: AIML 2002. (2002) 149–184

13. Círstea, C.: A compositional approach to defining logics for coalgebras. Theor. Comput. Sci. **327**(1-2) (2004) 45–69

14. Círstea, C., Pattinson, D.: Modular construction of complete coalgebraic logics. Theor. Comput. Sci. **388**(1-3) (2007) 83–108
15. Goldblatt, R.: Final coalgebras and the hennessy-milner property. Ann. Pure Appl. Logic **138**(1-3) (2006) 77-93

16. Kupke, C., Leal, R.A.: Characterising behavioural equivalence: Three sides of one coin. In Kurz, A., Lenisa, M., Tarlecki, A., eds.: CALCO 2009, Proceedings. (2009) 97-112

17. Levy, P.B.: Final Coalgebras from Corecursive Algebras. In Moss, L.S., Sobocinski, P., eds.: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Volume 35 of LIPIcs., Schloss Dagstuhl (2015) 221-237

18. Schröder, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science **390**(2) (2008) 230-247

19. Kupke, C., Kurz, A., Venema, Y.: Stone coalgebras. Theoretical Computer Science **327**(4) (2004) 109-134

20. Moss, L.S., Viglizzo, I.D.: Final coalgebras for functors on measurable spaces. Inf. Comput. **204**(4) (2006) 610-636

21. Kupke, C., Kurz, A., Pattinson, D.: Algebraic semantics for coalgebraic modal logic. In Adámek, J., ed.: Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS). Volume 106 of Electronic Notes in Theoretical Computer Science. (2004)

22. Klin, B.: Coalgebraic modal logic beyond sets. ENTCS **173** (2007) 177-201

23. Jacobs, B., Sokolova, A.: Exemplaric expressivity of modal logics. J. Log. Comput. **20**(5) (2010) 1041-1068

24. Dahlqvist, F., Kurz, A.: The positivication of coalgebraic logics. In Bonchi, F., König, B., eds.: CALCO 2017. Volume 72 of LIPIcs. (2017) 9:1-9:15

25. Klin, B.: Bialgebraic methods and modal logic in structural operational semantics. Inf. Comput. **207**(2) (2009) 237-257

26. Klin, B., Rot, J.: Coalgebraic trace semantics via forgetful logics. Logical Methods in Computer Science **12**(4) (2016)

27. Jacobs, B.: Trace semantics for coalgebras. ENTCS **106** (2004) 167-184

28. Rutten, J.: Relators and Metric Bisimulation (Extended Abstract). Electronic Notes in Theoretical Computer Science **11** (1998) 1-7

29. Kupke, C., Venema, Y.: Coalgebraic automata theory: Basic results. Logical Methods in Computer Science **4**(4) (2008)

30. Kupke, C., Kurz, A., Venema, Y.: Completeness for the coalgebraic cover modality. Logical Methods in Computer Science **8**(3) (2012)

31. Bílková, M., Palmigiano, A., Venema, Y.: Proof systems for Moss' coalgebraic logic. Theor. Comput. Sci. **549** (2014) 36-60

32. Santocanale, L.: Completions of $\mu$-algebras. Annals of Pure and Applied Logic **154**(1) (2008) 27-50

33. Venema, Y.: Automata and fixpoint logics: a coalgebraic perspective. Inf. Comp. **204** (2006) 637-678

34. Fontaine, G., Leal, R., Venema, Y.: Automata for coalgebras: an approach using predicate liftings. In: Proc. ICALP 2010. Volume 6199 of Lecture Notes in Computer Science., Springer (2010) 381-392

35. Círstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic $\mu$-calculus. Logical Methods in Computer Science **7**(3) (2011)

36. Schröder, L., Pattinson, D.: PSPACE Bounds for Rank-1 Modal Logics. ACM Trans. Comput. Logic **10**(2) (2009) 13:1-13:33

37. Santocanale, L., Venema, Y.: Completeness for flat modal fixpoint logics. Ann. Pure Appl. Logic **162**(1) (2010) 55-82

38. Schröder, L., Venema, Y.: Flat coalgebraic fixed point logics. In Gastin, P., Laroussinie, F., eds.: CONCUR 2010. Volume 6269 of LNCS. (2010) 524-538
39. Hansen, H.H., Kupke, C.: Weak completeness of coalgebraic dynamic logics. In Matthes, R., Mio, M., eds.: FICS 2015. (2015) 90–104

40. Enqvist, S., Seifan F., Venema, Y.: Completeness for coalgebraic fixpoint logic. In: CSL 2016. (2016) 7:1–7:19

41. Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Parity games and automata for game logic. In: DALI 2017. Volume 10669 of LNCS., Springer (2018) 115–132

42. Bezhanishvili, N., Kupke, C.: Games for topological fixpoint logic. In Cantone, D., Delzanno, G., eds.: GandALF 2016. Volume 226 of EPTCS. (2016) 46–60

43. Barlocco, S., Kupke, C.: Angluin learning via logic. In Artëmov, S.N., Nerode, A., eds.: LFCS 2018. Volume 10703 of LNCS. (2018) 72–90

44. Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation **75**(2) (1987) 87 – 106

45. Ghani, N., Kupke, C., Lambert, A., Forsberg, F.N.: A compositional treatment of iterated open games. CoRR abs/1711.07968 (2017)

46. Ghani, N., Hedges, J.: A compositional approach to economic game theory. CoRR abs/1603.04641 (2016)