informatics

Coalgebraic Logic: Expanding the Scope

We are currently looking for a Postdoc (3 years in Leicester) and a PhD student (3 years in Birmingham).

Project title: Coalgebraic Logic: Expanding the Scope

Background: Coalgebra

Logic plays a fundamental role in Computer Science. At the most basic level, Boolean logic is used to design the circuits we use every day in our computers. At the higher end, the tasks that computers perform need to conform to specifications expressed in logics suitable for programmers, analysts or even other computational devices. Such specification logics have to be able to express many different concepts such as time, knowledge, space, mobility, communication, probability, conditionals etc. Bespoke logics for each of these concepts exist and are studied under the umbrella of Modal Logic.

In any substantial application of Modal Logic to the specification of a system, the need to combine different logics will arise, each logic accounting for, eg, one of the aspects mentioned above. The need then arises to deal with these logics in a uniform and modular way. Not all of these logics have a standard Kripke semantics, but in all cases, the semantics can be considered to be coalgebraic. Coalgebras generalise the standard Kripke semantics of modal logic to encompass notions such as neighbourhood frames, Markov chains, topological spaces, etc.

Moreover, Coalgebra is a concept from Category Theory. Category Theory describes mathematical constructions via universal properties, which makes the constructions available in many different siutations in mathematics, logic, and computer science. In particular, the category theoretic nature of Coalgebras allows us to tackle the modularity problem using category theoretic constructions. One of the benefits of category theory is that these constructions, because of their generality, apply to specification languages and to their semantic models.

To summarise, Coalgebraic Logic combines Modal Logic with Coalgebra. This generalises modal logics from Kripke frames to coalgebras and makes category theoretic methods and constructions available in Modal Logic.

Aims: Expanding the Scope

Coalgebraic Logic can be traced back to 1997 when the first draft of Moss's paper with the same title was circulated. Since then, it has been developed by a number of researchers. Just now, Coalgebraic Logic is about to establish itself as an own area. Whereas much of the current work in Coalgebraic Logic aims at exploiting the current achievements towards more applications, this project starts from the following two observations:

First, Coalgebraic logic did not yet make use of many of the important developments that have taken place in Modal Logic. Two of these developments are:
• the relationship between Modal Logic and First-Order Logic;
• the uniform treatment of classes of modal logics.
Second, there exist many parallel developments in Modal Logic and Domain Theory. Some of the relationships have only recently become clear, through the connection of both areas with Coalgebra. We therefore plan to
• generalise methods from Modal Logic so that they can be applied to the logics arising in Domain Theory.

The project team

This is a joint project between Dr Alexander Kurz (University of Leicester) and Prof Achim Jung (University of Birmingham).

How to apply for the Postdoc (Deadline: 22 July 2009)

Go to the Vacancy Search of the University of Leicester and search for "Department of Computer Science" and/or Reference "SEN00006".

Questions on the project: email to Alexander Kurz.