Coalgebra-based generic decision procedures and complexity bounds for modal and hybrid logics (GenMod)

Modal logics and various extensions of the basic modal language, e.g. hybrid languages that provide expressive means for reasoning about individuals and fixed point languages that capture different forms of temporal development, traditionally play a central role in computer science, in particular in the analysis of reactive systems and in knowledge representation. In both areas, there has been a notable tendency to move beyond the classical Kripke-style relational interpretation of modalities towards more elaborate system types, such as game-based, probabilistic, or preferential systems, giving rise, e.g., to alternating-time temporal logic, probabilistic description logics, and non-monotonic conditional logics, which obey rather different laws than relational modal logics. Coalgebraic logic provides a framework in which a wide variety of such logics can be treated in a semantically uniform manner, and indeed even allows for the development of generic algorithms and an ensuing generic complexity analysis. The current project is aimed at further extending and deepening the algorithmic foundations of coalgebraic modal logic, in particular towards iterative logics, fixed point logics, decidable fragments of coalgebraic first-order logics, and many-dimensional coalgebraic logics. The generic algorithms will be combined with a range of generic heuristic optimization strategies to obtain an efficient reasoner for coalgebraic temporal and description logics.