Named Models in Coalgebraic Hybrid Logic

Modal logics have traditionally played a central role in Computer Science, appearing, e.g., in the guise of temporal logics, program logics such as PDL, epistemic logics, and later as description logics. The development of modal logics has seen extensions along (at least) two axes: the enhancement of the expressive power of basic (relational) modal logic on the one hand, and the continual extension, beyond the purely relational realm, of the class of structures described using modal logics on the other hand. Hybrid logic falls into the first category, extending modal logic with the ability to reason about individual states in models. This feature, originally suggested by Prior and first studied in the context of tense logics and PDL (see [5] for references), is of particular relevance in knowledge representation languages and as such has found its way into modern description logics, where it is denoted by the letter O in the standard naming scheme [2]. Extensions along the second axis - semantics beyond Kripke structures and neighbourhood models - include various probabilistic modal logics, interpreted over probabilistic transition systems, graded modal logic over multigraphs [8], conditional logics over selection function frames [6], and coalition logic [17], interpreted over so-called game frames. As a unifying semantic bracket covering all these logics and many further ones, coalgebraic modal logic has emerged ([7] gives a survey). The scope of coalgebraic modal logic has recently been expanded to encompass nominals; we refer to the arising class of logics as coalgebraic hybrid logics.