Workshop on Coalgebra and Logic
Date: 28-29 May 2009
Thursday, May 28
Friday, May 29
Title: Generalized Esakia duality
I will introduce partial Esakia morphisms, well partial Esakia morphisms, and strong partial Esakia morphisms between Esakia spaces and show that they provide the dual description of $(\wedge,\to)$-homomorphisms, $(\wedge,\to,0)$-homomorphisms, and $(\wedge,\to,\vee)$-homomorphisms between Heyting algebras, thus establishing a generalization of Esakia duality.
Title: Stone Duality for bitopological spaces
Samson Abramsky promoted the idea to use Stone duality to connect denotational semantics for programming languages with program logics. He developed a fairly specialised theory that was applicable to so-called Scott-domains (and SFP objects). In joint work with Drew Moshier, we found that the theory becomes much more elegant if carried out for stably compact spaces. More recently, we discovered that our duality (and the resulting logic) can usefully be expressed for bitopological spaces. This sheds new light on the logical set-up but, surprisingly, also on the classical dualities of Stone for Boolean algebras and distributive lattices.
Title: Trace Logics for Semiring Monads
(Joint work with Alexander Kurz)
Recently, coalgebraic logics have seen much attention as means to characterise points in Set-based coalgebras precisely up to bisimilarity. With the introduction of a uniform definition of trace semantics for coalgebras structured in the branching type given by a monad, the question was raised for a logic which describes points in such coalgebras adequately and expressively up to trace equivalence.
In this talk I will present recent work with Alexander Kurz on this question. We consider coalgebras on Set with branching given by evaluation in a fixed semiring, which defines a semiring monad. The trace semantics of such coalgebras is given by final sequence induction in the Kleisli-category, which in this case happens to be the category of freely generated semimodules. We then obtain trace logics and its semantics as transposes of respectively final coalgebra and final coalgebra morphism along the Morita adjunction induced by the semiring under consideration.
Title: Final Coalgebras and the Hennessy-Milner property
(Joint work with Raul Leal)
The notion of behavioural equivalence is central to the theory of coalgebras. In my talk will relate three different, but equivalent, ways to characterise behavioural equivalence for set coalgebras. These are: using final coalgebras, using coalgebraic languages that have the Hennessy- Milner property and using coalgebraic languages that have ``logical congruences''. In particular, I will present a straightforward construction of the final T-coalgebra of a set functor using a given logical language that has the Hennessy-Milner property with respect to the class of T-coalgebras. Finally I will discuss generalizations to coalgebras over other categories.
Title: Towards Universal Algebra for Nominal Sets
(Joint work with Daniela Petrisan)
Starting from the observation that nominal sets (in the sense of Gabbay and Pitts) are a full reflective subcategory of a category of algebras, we propose to use standard universal algebra to do algebra over nominal sets. For example, it is possible to adapt the standard proof of Birkhoff's HSP theorem to nominal algebra. We compare this with J.M.Gabbay's Nominal Algebra and the HSP-theorem.
Title: Coalgebraic Tableaux
Formulae of multisorted coalgebraic modal logics, which may contain fixpoints, universal programs, nominals or other features, are often thought of as partial observations satisfied in some model. However we note that they may also be seen as elements of the respective final coalgebra, in the sense that coalgebraic tableaux algorithms construct satisfying models from these formulae. Recently Silva, Bosangue and Rutten have presented generic fixpoint expressions together with a generalisation of both Kleene's theorem for regular expressions and the complete equational logic of Kleene algebra; this covers Mealy machines and Kleene algebras with tests amongst others. We will show that this work is an instantiation of this observation, thereby obtaining a generic decision procedure and a considerable generalisation beyond the Kripke polynomial coalgebra case they presented. We will also discuss the framework of multisorted coalgebraic hybrid logic with the universal modality, which amongst other things provides a generic framework for Description Logic (DL) and even appears to provide a new "canonical" tableaux for the well-studied relational case. An example application outside DL lies in the area of norm-governed multi-agent systems.
Title:The Coalgebraic mu-calculus
(Joint work with Corina Cirstea and Clemens Kupke)
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic μ-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games.
Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic μ-calculus and for an extension of coalition logic with fixpoints.
Title: A Duality Theorem for Real Commutative C* Algebras
(Joint Work with Drew Moshier)
Real commutative C* algebras have come under attention in theoretical computer science as an abstraction of the notion of ``test'' or ``observation.'' Another way to think about observations has a longer history in domain theory. The open sets of a Scott topology are regarded as forming a logic of observable properties. The two approaches are related via the two Stone duality theorems: C* algebras vs. compact Hausdorff spaces on one hand, and Boolean algebras vs. Stone spaces on the other. We investigate the connections between the `logical' view and the `real ring' view, giving a direct proof for the equivalence between the category of C* algebras and the category of skew frames with negation. The latter appears in the work of Jung and Moshier on the bitopological nature of Stone duality. Consequently, we can prove that the category of C* algebras and the category of proximity lattices with negation are dually equivalent, without going through the construction of spaces.
Title: Coalgebras and bisimulations, for name-passing process calculi
Title: Automata for nominal calculi
History Dependent automata (HDA) provide a syntax-independent operational models where states and transitions of classical automata are enriched with (finite sets of) names and symmetries on them. The formal basis upon wich HDA have been built are named sets which turn to be equivalent to nominal sets. HDA have been used to check semantic equivalences on nominal calculi (e.g., bisimulation of pi-calculus and hyperbisimulation of Fusion calculus). This talk will present the algorithm for minimising HDA which is used to check the semantic equivalence of processes.