Computational Complexity of a Core Fragment of Halpern-Shoham Logic

Author Przemyslaw Andrzej Walega

Thumbnail PDF


  • Filesize: 0.51 MB
  • 18 pages

Document Identifiers

Author Details

Przemyslaw Andrzej Walega
  • University of Oxford, United Kingdom, University of Warsaw, Poland

Cite AsGet BibTex

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)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Temporal Logic
  • Interval Logic
  • Computational Complexity
  • Hybrid Logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. James F Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. Google Scholar
  2. Carlos Areces, Patrick Blackburn, and Maarten Marx. The computational complexity of hybrid temporal logics. Logic Journal of IGPL, 8(5):653-679, 2000. Google Scholar
  3. Patrick Blackburn. Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of the IGPL, 8(3), 2000. Google Scholar
  4. Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal Logic, volume 53. Cambridge University Press, 2002. Google Scholar
  5. Davide Bresolin, Dario Della Monica, Angelo Montanari, Pietro Sala, and Guido Sciavicco. Interval temporal logics over strongly discrete linear orders: expressiveness and complexity. Theoretical Computer Science, 560:269-291, 2014. Google Scholar
  6. Davide Bresolin, Dario Della Monica, Angelo Montanari, Pietro Sala, and Guido Sciavicco. The light side of interval temporal logic: The Bernays-Schönfinkel’s fragment of CDT. Annals of Mathematics and Artificial Intelligence, 71:11-39, 2014. Google Scholar
  7. Davide Bresolin, Dario Della Monica, Angelo Montanari, Pietro Sala, and Guido Sciavicco. On the complexity of fragments of the modal logic of Allen’s relations over dense structures. In LATA, pages 511-523, 2015. Google Scholar
  8. Davide Bresolin, Agi Kurucz, Emilio Muñoz-Velasco, Vladislav Ryzhikov, Guido Sciavicco, and Michael Zakharyaschev. Horn fragments of the Halpern-Shoham interval temporal logic. ACM Transactions on Computational Logic (TOCL), 18(3):22:1-22:39, 2017. Google Scholar
  9. Davide Bresolin, Emilio Muñoz-Velasco, and Guido Sciavicco. Sub-propositional fragments of the interval temporal logic of Allen’s relations. In European Workshop on Logics in Artificial Intelligence, pages 122-136. Springer, 2014. Google Scholar
  10. Davide Bresolin, Emilio Munoz-Velasco, and Guido Sciavicco. On the complexity of fragments of Horn modal logics. In Temporal Representation and Reasoning (TIME), 2016 23rd International Symposium on, pages 186-195. IEEE, 2016. Google Scholar
  11. Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco, et al. Interval temporal logics: a journey. Bulletin of EATCS, 3(105), 2013. Google Scholar
  12. Michael Fisher. A resolution method for temporal logic. In IJCAI, volume 91, pages 99-104, 1991. Google Scholar
  13. Valentin Goranko, Angelo Montanari, and Guido Sciavicco. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14(1-2):9-54, 2004. Google Scholar
  14. Joseph Y Halpern and Yoav Shoham. A propositional modal logic of time intervals. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 279-292. Computer Society Press, 1986. Google Scholar
  15. Joseph Y Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM (JACM), 38(4):935-962, 1991. Google Scholar
  16. Roman Kontchakov, Laura Pandolfo, Luca Pulina, Vladislav Ryzhikov, and Michael Zakharyaschev. Temporal and spatial OBDA with many-dimensional Halpern-Shoham logic. In IJCAI, pages 1160-1166, 2016. Google Scholar
  17. Linh A Nguyen. On the complexity of fragments of modal logics. Advances in Modal logic, 5:318-330, 2004. Google Scholar
  18. Christos H Papadimitriou. Computational Complexity. John Wiley and Sons Ltd., 2003. Google Scholar
  19. Yde Venema. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. Google Scholar
  20. Przemysław A Wałęga. Computational complexity of a hybridized Horn fragment of Halpern-Shoham logic. In Indian Conference on Logic and Its Applications, pages 224-238. Springer, 2017. Google Scholar
  21. Przemysław A Wałęga. On expressiveness of Halpern-Shoham logic and its Horn fragments. In LIPIcs-Leibniz International Proceedings in Informatics, volume 90. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail