Teaching Projects Research PhD Topics Talks Publications Software

Coalgebraic Modal Logic: Fixpoints and Nested Modalities

Principal InvestigatorDirk Pattinson
Start DateMar 1, 2008
Value£ 311,532
Sponsor Engineering and Physical Sciences Research Council (EPSRC)
Reference EP/F031173/1
Research Associate Clemens Kupke


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.


Informal Enquiries and Job Advert

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

Dirk Pattinson [check HTML] [check CSS]