Dirk Pattinson

The Australian National University
Research School of Computer Science
Logic and Computation Group

RSISE Buliding 115
The Australian National University
Canberra ACT 0200
Australia

E dirk.pattinson@anu.edu.au
T +61 (0)2 6125 8612
F +61 (0)2 6125 8651

Coalgebraic Modal Logic: Fixpoints and Nested Modalities

Summary

Coalgebraic Logic is a paradigm that subsumes a large class of structurally different modal logics, such as e.g. Coalition Logic, graded and probabilistic modal logic and conditional logic, classical and monotone modal logic as well as the modal logic K. The goal of this project is to extend the scope of the coalgebraic approach by considering two extensions to the basic setup: frame conditions, in particular those that feature nested modalities, and fixpoints.

Research Description

Modal logic is a formal framework for reasoning about change. Applications of modal logics are abundant in computer science and related disciplines, and a multitude of different logics have been studied in a variety of application contexts. Apart from classical applications in the field of concurrent, mobile and probabilistic systems, modal logics are used in artificial intelligence, e.g. in the context of reasoning with uncertainty and -- in the shape of description logics -- in the field of knowledge representation. Modal logics are also employed to reason about games and coalitional power in multi-agent systems. In economics, they have been used to describe probabilistic information shared by interacting agents whereas e.g. deontic logic, the logic of obligation and permission is studied in philosophy. The study of all of these logics centres around a number of recurring questions, including completeness (``are all valid statements formally derivable?''), decidability (``is the logic amenable to automated reasoning?'') and complexity (``what resources are required to mechanise the logic?''), which are usually studied for each logic individually. Rather than addressing these questions in a per-logic basis, it is clearly desirable to conduct the studies in a uniform framework that encompasses the greatest possible number of concretely given logics as special cases. The proposed research investigates and extends a generic framework -- coalgebraic modal logic -- that encompasses a large class of modal logics as specific examples, including all instances mentioned above. The genericity of the approach will lead to software tools that are not only more reliable but also and easier to design, implement and to maintain.

Objectives

• Development of a coalgebraic semantics for modal logics that incorporate nested modalities and/or fixpoints
• Generic (soundness and) completeness theorems that connect the above logics with their coalgebraic semantics
• Construction of uniform algorithms to decide the satisfiability problem so that the decidability problem induced by a concretely given logic can be solved by an appropriate instantiation
• Evaluation of the ensuing algorithms on a theoretical level (tight complexity bounds) and from a practical viewpoint (prototypical implementation and comparison with other techniques)
• Investigation of compositional techniques to
• obtain both new theoretical results (completeness, decidability) and practical decision procedures for combined logics.

Informal Enquiries and Job Advert

Email dirk@doc.ic.ac.uk for informal enquiries. The job advert can be found here.