Alexandru Baltag

Title: Universal Set Theory is the Canonical Model for Infinitary Modal Logic

Abstract: In this talk, I will present some older work on modeling and axiomatizing a non-classical, non-wellfounded set theory with a universal set and very strong comprehension and topological closure properties, by using infinitary modal logic. The model is essentially given by the canonical model construction for a modal language with conjunctions of size less than kappa, where kappa is a weakly compact cardinal. The axiomatization is based on a natural extension of Aczel's Antifoundation Axiom, whose most direct formulation uses infinitary modal logic. The notion of observational equivalence, given by elementary equivalence with respect to infinitary modal logic (and close, but not equivalent, to the standard notion of bisimulation) plays a central role. The resulting model is a kind of Cauchy completion of Aczel's non-wellfounded universem and, in certain assumptions, is isomorphic with the ``topological set theory" model of Forti and Honsell, first proposed as a model for the so-called ``Positive Comprehension Axiom". I show how this theory ``solves" the classical paradoxes and can be used to formalize a ``reflexive" category of all categories, as well as prove fixed point theorems relating set-theoretic recursion and corecursion. I speculate about the model-theoretic, topological and coalgebraic consequences of this work.

Nick Bezhanishvili

Title: The Final Coalgebra for the Vietoris Functor

(Joint work with Alexander Kurz)

Abstract: In this talk, I will describe the final coalgebra for the Vietoris functor.

Corina Cirstea

(Joint work with M. Sadrzadeh)

Title: Towards a Modular Coalgebraic Approach to Model-based Verification

Abstract: I will consider a variation of the notion of logical F-automata operating on F-coalgebras, as introduced by Venema (2004), and present some initial results towards using such automata for model-checking coalgebraic models.

Martin Escardo

Title: Stably Compact Spaces

Abstract: Stably compact spaces were discovered independently by a number of people in different guises, with more guises uncovered after their initial identification. These spaces can be traced back to the work of M. Stone (1937) on the representation of distributive lattices by spectral spaces, of L. Nachbin (1950) on compact ordered topological spaces, and of H. Priestley (1972) on representation of distributive lattices by ordered Stone spaces. This talk will be a tour of a dozen pieces of work on stably compact spaces. In particular, I'll present many equivalent characterizations of the notion/category of stably compact spaces.

Helle Hvid Hansen

Title: Coalgebras for Sequential Transducers

Abstract: Sequential transducers are deterministic finite state machines which compute partial word functions f:A^∗ → B^∗. They have applications in coding theory and language processing, and they form an interesting generalisation of both deterministic finite automata and Mealy machines. It is known that DFA's and Mealy machines can be viewed as coalgebras in such a way that the coalgebraic semantics coincides with the traditional automaton semantics. The questions arise whether this coalgebraic framework can be generalised to sequential transducers, and whether a coalgebraic perspective can provide useful insights into existing results and constructions. In my talk I will describe some initial findings of this line of investigation.

Ichiro Hasuo

Title: Coalgebras in Kleisli Categories

Abstract: The theory of coalgebras has been a big success as a mathematical framework to reason about state-based reactive systems. As a base category, the category Sets of sets and functions is conventionally taken: then the coalgebraic notions capture semantics of systems modulo bisimilarity. Namely, in Sets,
- a coalgebra is a system, - a morphism of coalgebras is a map which preserves behavior modulo bisimulation, that is, a functional bisimulation,
- via coinduction we obtain a semantics of systems modulo bisimilarity.

Then we may ask the following questions:
- If we take a base category different from Sets, what computational meaning do the coalgebraic notions (morphisms, coinduction, etc.) have?
- If we are interested in a semantics of systems which is different from (i.e. coarser than) bisimilarity, how can we capture it coalgebraically?

In this talk we shall give one answer to these questions, proposing a Kleisli category for a monad as an alternative base category. There the coalgebraic notions capture trace semantics of systems. More precisely, in a Kleisli category,
- a coalgebra is a system,
- a lax/oplax morphism of coalgebras is a forward/backward simulation between systems, and,
- via coinduction we obtain the trace semantics of systems.
By replacing monads we can handle both non-deterministic and probabilistic branching in a uniform manner.

Hence we identify a new application field of coalgebras. This also demonstrates the power of categorical--in particular coalgebraic--methods in computer science: the theory of coalgebras is robust against change of base categories, i.e. change of semantics we want to capture.

References:
[1] Ichiro Hasuo, Bart Jacobs and Ana Sokolova.
Generic Trace Theory. In CMCS 2006.
[2] Ichiro Hasuo.
Generic Forward and Backward Simulations. In CONCUR 2006.

Ian Hodkinson

Title: Axiomatising the Modal Logic of Affine Planes

Bartek Klin

Title: Modal Logics for Coalgebras and Bialgebras on Categories other than Set

Abstract: I will describe some ongoing work aimed at generalizing coalgebraic modal logic to various categories, based on arbitrary contravariant adjunctions rather than dualities. I will also show how the logical approach for coalgebras can be extended to processes with syntax (i.e., bialgebras), possibly leading to new techniques for finding well-behaved frameworks for structural operational semantics.

Clemens Kupke

Title: The Finite Model Property of Coalgebraic Fixed Point Logics

(Joint work with Yde Venema)

Abstract: A coalgebra automaton is a finite automaton that may accept or reject a given pointed coalgebra. Automata that operate on infinite words, trees and graphs can be seen as examples of coalgebra automata.

In my talk, I will sketch a solution to the non-emptiness problem of coalgebra automata: every automaton that accepts some pointed coalgebra accepts a pointed coalgebra that has a finite carrier set. This implies that coalgebraic fixed point logics, and in particular the modal mu calculus, have the finite model property.

Alexander Kurz

Title: A Categorical Characterisation of Modal Axiomatisations of Rank 1

(Joint work with Jiri Rosicky)

Abstract: We show that modal logics that have an axiomatisation of rank 1 correspond precisely to endofunctors on the category BA of Boolean algebras. An immediate corollary is that there is a strongly complete logic for T-coalgebras for any functor T on Stone spaces that is determined by its action on finite Stone spaces. We will also indicate how to obtain from this strong completeness results for coalgebras based on sets rather than Stone spaces.

Frank Wolter

Title: Conservative Extensions in Modal Logic

Abstract: A theory T is said to be a conservative extension of a theory T′ if any consequence of T, which only uses symbols from T′, is a consequence of T′ as well. This notion plays an important role in mathematical logic and the foundations of mathematics.

Rather surprisingly, in modal logic the notion of conservative extension has hardly been investigated. Indeed, modal theories - similarly to first-order theories - have become fundamental tools for representing various domains. For example, in epistemic logic, modal theories represent the (possibly introspective) knowledge of an agent; in temporal logic, theories serve as specifications of concurrent systems; in description logic, theories (called TBoxes) are ontologies used to fix the terminology of an application domain, etc. In all these examples, the notion of a conservative extension can be used to compare different theories and derive important information about their relation to each other. For instance, a description logic ontology T′ can be regarded as a `safe' extension of another description logic ontology T if, and only if, T′ is a conservative extension of T.

One of the main reasons for using modal logic instead of full first-order logic in the applications above is that reasoning in modal logic is often decidable. To employ the notion of conservative extension for modal logics, it is therefore crucial to analyse the algorithmic problem of deciding whether one modal theory is a conservative extension of another modal theory.

In this talk, we investigate the notion of conservative extension for a number of basic modal logics and, in particular, determine the computational complexity of the conservativeness problem for these logics. We will also discuss the relation to uniform interpolation and bisimulation quantifiers.

We begin by showing that deciding non-conservativeness is NExpTime-hard for all modal logics which have rooted frames with more than N successors of the root, for any finite N. This result covers almost all standard modal logics, for example, K, S4, and S5. Next, we consider the modal logic S5 and show that in this case non-conservativeness is NExpTime-complete by proving that one can construct a uniform interpolant of exponential size in exponential time (in the size of a given formula) and using the fact that S5-satisfiability is decidable in NP. A slightly different technique is used to prove that for K non-conservativeness is NExpTime-complete. Finally, we consider the conservativeness problem for S4 and establish an ExpSpace upper bound.

The talk is based on joint work with Silvio Ghilardi, Carsten Lutz, and Michael Zakharyaschev.