TY - GEN
T1 - Coalgebraic hybrid logic
AU - Myers, Rob
AU - Pattinson, Dirk
AU - Schröder, Lutz
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350656392&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-00596-1_11
DO - 10.1007/978-3-642-00596-1_11
M3 - Conference contribution
SN - 3642005950
SN - 9783642005954
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 137
EP - 151
BT - Foundations of Software Science and Computational Structures - 12th International Conference, FOSSACS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc.
T2 - 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
Y2 - 22 March 2009 through 29 March 2009
ER -