Coalgebraic Hybrid Logic (bibtex)

by Rob Myers, Dirk Pattinson and Lutz Schröder

Abstract:

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.

Reference:

Rob Myers, Dirk Pattinson and Lutz Schröder: Coalgebraic Hybrid Logic, In Luca de Alfaro, ed.: Foundations of Software Science and Computation Structures (FOSSACS 2009), Lecture Notes in Computer Science, vol. 5504, pp. 137–151, Springer, 2009. [preprint]

Bibtex Entry:

@InProceedings{MyersEA09,
  author = {Rob Myers and Dirk Pattinson and Lutz Schr{\"o}der},
  title = {Coalgebraic Hybrid Logic},
  year = {2009},
  editor = {Luca de Alfaro},
  booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2009)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5504},
  pages = {137-151},
  keywords = {coalgebra hybrid logic decision procedures polynomial space hilbert gentzen sequent tableaux},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/chl.pdf"> [preprint] </a>},
  abstract = { 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.},
}