Coalgebraic Hybrid Logic

Rob Myers, Dirk Pattinson, Lutz Schröder

In: Luca de Alfaro (Hrsg.). Foundations of Software Science and Computation Structures. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS-09) 12th befindet sich Joint European Conferences on Theory and Practice of Software, ETAPS 2009 March 22-25 York United Kingdom Seiten 137-151 Lecture Notes in Computer Science (LNCS) 5504 ISBN 0302-9743 Springer 2009.


We introduce a generic framework for hybrid logics, i.e. modal logics additionally featuring nominals and satisfaction operators, thus providing the necessary facilities for reasoning about individual states in a model. This framework, coalgebraic hybrid logic, works at the same level of generality as coalgebraic modal logic, and in particular subsumes, besides normal hybrid logics such as hybrid K, a wide variety of logics with non-normal modal operators such as probabilistic, graded, or coalitional modalities and non-monotonic conditionals. We prove a generic finite model property and an ensuing weak completeness result, and we give a semantic criterion for decidability in PSPACE. Moreover, we present a fully internalised PSPACE tableau calculus. These generic results are easily instantiated to particular hybrid logics and thus yield a wide range of new results, including e.g. decidability in PSPACE of probabilistic and graded hybrid logics.


Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence