Coalgebraic Modal Logic: Fixpoints and Nested Modalities

点击翻译按钮获取中文摘要

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 ofdescription 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 ofconcretely 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.