3 Search Results for "Walega, Przemyslaw Andrzej"

Document
DOI: 10.4230/LIPIcs.TIME.2019.4
A Modal Logic for Subject-Oriented Spatial Reasoning

Authors: Przemysław Andrzej Wałęga and Michał Zawidzki

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
We present a modal logic for representing and reasoning about space seen from the subject’s perspective. The language of our logic comprises modal operators for the relations "in front", "behind", "to the left", and "to the right" of the subject, which introduce the intrinsic frame of reference; and operators for "behind an object", "between the subject and an object", "to the left of an object", and "to the right of an object", employing the relative frame of reference. The language allows us to express nominals, hybrid operators, and a restricted form of distance operators which, as we demonstrate by example, makes the logic interesting for potential applications. We prove that the satisfiability problem in the logic is decidable and in particular PSpace-complete.
Cite as

Przemysław Andrzej Wałęga and Michał Zawidzki. A Modal Logic for Subject-Oriented Spatial Reasoning. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 4:1-4:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{walega_et_al:LIPIcs.TIME.2019.4,
  author =	{Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej and Zawidzki, Micha{\l}},
  title =	{{A Modal Logic for Subject-Oriented Spatial Reasoning}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.4},
  URN =		{urn:nbn:de:0030-drops-113622},
  doi =		{10.4230/LIPIcs.TIME.2019.4},
  annote =	{Keywords: spatial logic, modal logic, subject-oriented, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.TIME.2018.23
Computational Complexity of a Core Fragment of Halpern-Shoham Logic

Authors: Przemyslaw Andrzej Walega

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

Abstract
Halpern-Shoham logic (HS) is a highly expressive interval temporal logic but the satisfiability problem of its formulas is undecidable. The main goal in the research area is to introduce fragments of the logic which are of low computational complexity and of expressive power high enough for practical applications. Recently introduced syntactical restrictions imposed on formulas and semantical constraints put on models gave rise to tractable HS fragments for which prototypical real-world applications have already been proposed. One of such fragments is obtained by forbidding diamond modal operators and limiting formulas to the core form, i.e., the Horn form with at most one literal in the antecedent. The fragment was known to be NL-hard and in P but no tight results were known. In the paper we prove its P-completeness in the case where punctual intervals are allowed and the timeline is dense. Importantly, the fragment is not referential, i.e., it does not allow us to express nominals (which label intervals) and satisfaction operators (which enables us to refer to intervals by their labels). We show that by adding nominals and satisfaction operators to the fragment we reach NP-completeness whenever the timeline is dense or the interpretation of modal operators is weakened (excluding the case when punctual intervals are disallowed and the timeline is discrete). Moreover, we prove that in the case of language containing nominals but not satisfaction operators, the fragment is still NP-complete over dense timelines.
Cite as

Przemyslaw Andrzej Walega. Computational Complexity of a Core Fragment of Halpern-Shoham Logic. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 23:1-23:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{walega:LIPIcs.TIME.2018.23,
  author =	{Walega, Przemyslaw Andrzej},
  title =	{{Computational Complexity of a Core Fragment of Halpern-Shoham Logic}},
  booktitle =	{25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-089-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{120},
  editor =	{Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.23},
  URN =		{urn:nbn:de:0030-drops-97880},
  doi =		{10.4230/LIPIcs.TIME.2018.23},
  annote =	{Keywords: Temporal Logic, Interval Logic, Computational Complexity, Hybrid Logic}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.22
On Expressiveness of Halpern-Shoham Logic and its Horn Fragments

Authors: Przemyslaw Andrzej Walega

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Abstract: Halpern and Shoham's modal logic of time intervals (HS in short) is an elegant and highly influential propositional interval-based logic. Its Horn fragments and their hybrid extensions have been recently intensively studied and successfully applied in real-world use cases. Detailed investigation of their decidability and computational complexity has been conducted, however, there has been significantly less research on their expressive power. In this paper we make a step towards filling this gap. We (1) show what time structures are definable in the language of HS, and (2) determine which HS fragments are capable of expressing: hybrid machinery, i.e., nominals and satisfaction operators, and somewhere, difference, and everywhere modal operators. These results enable us to classify HS Horn fragments according to their expressive power and to gain insight in the interplay between their decidability/computational complexity and expressiveness.
Cite as

Przemyslaw Andrzej Walega. On Expressiveness of Halpern-Shoham Logic and its Horn Fragments. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 22:1-22:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{walega:LIPIcs.TIME.2017.22,
  author =	{Walega, Przemyslaw Andrzej},
  title =	{{On Expressiveness of Halpern-Shoham Logic and its Horn Fragments}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.22},
  URN =		{urn:nbn:de:0030-drops-79307},
  doi =		{10.4230/LIPIcs.TIME.2017.22},
  annote =	{Keywords: Temporal Logic, Interval Logic, Expressiveness, Hybrid Logic}
}
  • Refine by Author
  • 2 Walega, Przemyslaw Andrzej
  • 1 Wałęga, Przemysław Andrzej
  • 1 Zawidzki, Michał

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 2 Hybrid Logic
  • 2 Interval Logic
  • 2 Temporal Logic
  • 1 Computational Complexity
  • 1 Expressiveness
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2017
  • 1 2018
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact