A road-map on complexity for hybrid logics

Carlos Areces; Patrick Blackburn; Maarten Marx

doi:10.1007/3-540-48168-0_22

A road-map on complexity for hybrid logics

Carlos Areces
, Patrick Blackburn
, Maarten Marx

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

78 Citations (Scopus)

Abstract

Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reasoning. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one. Our work falls into two parts. We first examine the basic hybrid language and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have pspace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from pspace to exptime. In the second part we turn to stronger hybrid languages in which it is possible to bind nominals. We prove a general expressivity result showing that even the weak form of binding offered by the ↓ operator easily leads to undecidability.

Original language	English
Title of host publication	Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings
Editors	Jörg Flum, Mario Rodriguez-Artalejo
Number of pages	15
Publisher	Springer
Publication date	1999
Pages	307-321
ISBN (Print)	3540665366, 9783540665366
DOIs	https://doi.org/10.1007/3-540-48168-0_22
Publication status	Published - 1999
Externally published	Yes
Event	13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999 - Madrid, Spain Duration: 20 Sept 1999 → 25 Sept 1999

Conference

Conference	13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999
Country/Territory	Spain
City	Madrid
Period	20/09/1999 → 25/09/1999

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1683
ISSN	0302-9743

Keywords

Computational complexity
Description logic
Labeled deduction
Modal and temporal logic

Access to Document

10.1007/3-540-48168-0_22

Citation Styles

Areces, Carlos ; Blackburn, Patrick ; Marx, Maarten. / A road-map on complexity for hybrid logics. Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings. editor / Jörg Flum ; Mario Rodriguez-Artalejo. Springer, 1999. pp. 307-321 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 1683).

@inproceedings{9325ceda5f5240b5b95298ad9fb8874e,

title = "A road-map on complexity for hybrid logics",

abstract = "Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reasoning. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one. Our work falls into two parts. We first examine the basic hybrid language and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have pspace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from pspace to exptime. In the second part we turn to stronger hybrid languages in which it is possible to bind nominals. We prove a general expressivity result showing that even the weak form of binding offered by the ↓ operator easily leads to undecidability.",

keywords = "Computational complexity, Description logic, Labeled deduction, Modal and temporal logic, Computational complexity, Description logic, Labeled deduction, Modal and temporal logic",

author = "Carlos Areces and Patrick Blackburn and Maarten Marx",

year = "1999",

doi = "10.1007/3-540-48168-0\_22",

language = "English",

isbn = "3540665366",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "307--321",

editor = "J{\"o}rg Flum and Mario Rodriguez-Artalejo",

booktitle = "Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings",

note = "13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999 ; Conference date: 20-09-1999 Through 25-09-1999",

}

Areces, C, Blackburn, P & Marx, M 1999, A road-map on complexity for hybrid logics. in J Flum & M Rodriguez-Artalejo (eds), Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1683, pp. 307-321, 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999, Madrid, Spain, 20/09/1999. https://doi.org/10.1007/3-540-48168-0_22

A road-map on complexity for hybrid logics. / Areces, Carlos; Blackburn, Patrick; Marx, Maarten.
Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings. ed. / Jörg Flum; Mario Rodriguez-Artalejo. Springer, 1999. p. 307-321 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 1683).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - A road-map on complexity for hybrid logics

AU - Areces, Carlos

AU - Blackburn, Patrick

AU - Marx, Maarten

PY - 1999

Y1 - 1999

N2 - Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reasoning. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one. Our work falls into two parts. We first examine the basic hybrid language and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have pspace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from pspace to exptime. In the second part we turn to stronger hybrid languages in which it is possible to bind nominals. We prove a general expressivity result showing that even the weak form of binding offered by the ↓ operator easily leads to undecidability.

AB - Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reasoning. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one. Our work falls into two parts. We first examine the basic hybrid language and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have pspace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from pspace to exptime. In the second part we turn to stronger hybrid languages in which it is possible to bind nominals. We prove a general expressivity result showing that even the weak form of binding offered by the ↓ operator easily leads to undecidability.

KW - Computational complexity

KW - Description logic

KW - Labeled deduction

KW - Modal and temporal logic

KW - Computational complexity

KW - Description logic

KW - Labeled deduction

KW - Modal and temporal logic

U2 - 10.1007/3-540-48168-0_22

DO - 10.1007/3-540-48168-0_22

M3 - Article in proceedings

AN - SCOPUS:84956862612

SN - 3540665366

SN - 9783540665366

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 307

EP - 321

BT - Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings

A2 - Flum, Jörg

A2 - Rodriguez-Artalejo, Mario

PB - Springer

T2 - 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999

Y2 - 20 September 1999 through 25 September 1999

ER -

Areces C, Blackburn P, Marx M. A road-map on complexity for hybrid logics. In Flum J, Rodriguez-Artalejo M, editors, Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings. Springer. 1999. p. 307-321. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 1683). doi: 10.1007/3-540-48168-0_22