Document Open Access Logo

Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes

Authors Laura Bozzelli, Angelo Montanari, Adriano Peron, Pietro Sala

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.9.pdf
  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

Laura Bozzelli
  • University of Napoli "Federico II", Italy
Angelo Montanari
  • University of Udine, Italy
Adriano Peron
  • University of Napoli "Federico II", Italy
Pietro Sala
  • University of Verona, Italy

Acknowledgements

The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.

Cite AsGet BibTex

Laura Bozzelli, Angelo Montanari, Adriano Peron, and Pietro Sala. Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TIME.2021.9

Abstract

In this paper, we establish Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality ⟨E⟩, for the "suffix" relation on pairs of intervals, and modality ⟨D⟩, for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes (⟨E⟩) or, symmetrically, the modality for prefixes (⟨B⟩) to the logic of sub-intervals (featuring only ⟨D⟩).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Interval temporal logic
  • Satisfiability
  • Model checking

Metrics

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

References

  1. J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. Google Scholar
  2. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption. In Proc. 44th ICALP, volume 80 of LIPIcs, pages 120:1-120:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.120.
  3. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy. Inf. Comput., 262(Part):241-264, 2018. URL: https://doi.org/10.1016/j.ic.2018.09.006.
  4. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison. ACM Trans. Comput. Log., 20(1):4:1-4:31, 2019. URL: https://dl.acm.org/citation.cfm?id=3281028.
  5. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Which fragments of the interval temporal logic HS are tractable in model checking? Theor. Comput. Sci., 764:125-144, 2019. URL: https://doi.org/10.1016/j.tcs.2018.04.011.
  6. L. Bozzelli, A. Montanari, and A. Peron. Complexity analysis of a unifying algorithm for model checking interval temporal logic. In Proc 26th TIME, volume 147 of LIPIcs, pages 18:1-18:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TIME.2019.18.
  7. L. Bozzelli, A. Montanari, A. Peron, and P. Sala. On a temporal logic of prefixes and infixes. In Proc. 45th MFCS, volume 170 of LIPIcs, pages 21:1-21:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.21.
  8. D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. The dark side of interval temporal logic: marking the undecidability border. Annals of Mathematics and Artificial Intelligence, 71(1-3):41-83, 2014. URL: https://doi.org/10.1007/s10472-013-9376-4.
  9. D. Bresolin, V. Goranko, A. Montanari, and P. Sala. Tableaux for Logics of Subinterval Structures over Dense Orderings. Journal of Logic and Computation, 20(1):133-166, 2010. URL: https://doi.org/10.1093/logcom/exn063.
  10. D. Bresolin, V. Goranko, A. Montanari, and G. Sciavicco. Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic, 161(3):289-304, 2009. URL: https://doi.org/10.1016/j.apal.2009.07.003.
  11. D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Interval Temporal Logics: a Journey. Bulletin of the EATCS, 105:73-99, 2011. URL: http://albcom.lsi.upc.edu/ojs/index.php/beatcs/article/view/98.
  12. V. Diekert and P. Gastin. First-order definable languages. In Logic and Automata, volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  13. E. A. Emerson and J. Y. Halpern. "Sometimes" and "not never" revisited: on branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  14. J. Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM, 38:279-292, 1991. URL: https://doi.org/10.1145/115234.115351.
  15. I. Hodkinson, A. Montanari, and G. Sciavicco. Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T. In CSL, volume 5213 of LNCS, pages 308-322. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_23.
  16. K. Lodaya. Sharpening the Undecidability of Interval Temporal Logic. In Proc. 6th ASIAN, LNCS 1961, pages 290-298. Springer, 2000. URL: https://doi.org/10.1007/3-540-44464-5_21.
  17. A. Lomuscio and J. Michaliszyn. An Epistemic Halpern-Shoham Logic. In Proc. 23rd IJCAI, pages 1010-1016. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6632.
  18. A. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class of EHS specifications. In Proc. 21st ECAI, volume 263 of Frontiers in Artificial Intelligence and Applications, pages 543-548. IOS Press, 2014. URL: https://doi.org/10.3233/978-1-61499-419-0-543.
  19. A. Lomuscio and J. Michaliszyn. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In Proc. 15th KR, pages 298-308. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12823.
  20. J. Marcinkowski and J. Michaliszyn. The Undecidability of the Logic of Subintervals. Fundam. Inform., 131(2):217-240, 2014. URL: https://doi.org/10.3233/FI-2014-1011.
  21. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. Acta Informatica, 53(6-8):587-619, 2016. URL: https://doi.org/10.1007/s00236-015-0250-1.
  22. A. Molinari, A. Montanari, and A. Peron. Model checking for fragments of Halpern and Shoham’s interval temporal logic based on track representatives. Inf. Comput., 259(3):412-443, 2018. URL: https://doi.org/10.1016/j.ic.2017.08.011.
  23. A. Montanari. Interval temporal logics model checking. In Proc. 23rd TIME, page 2. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/TIME.2016.32.
  24. B. Moszkowski. Reasoning About Digital Circuits. PhD thesis, Dept. of Computer Science, Stanford University, Stanford, CA, 1983. Google Scholar
  25. A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pages 46-57. IEEE, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  26. I. Pratt-Hartmann. Temporal propositions and their logic. Artificial Intelligence, 166(1-2):1-36, 2005. URL: https://doi.org/10.1016/j.artint.2005.04.003.
  27. P. Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. URL: https://doi.org/10.1007/BF00262866.
  28. L. J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, 1974. Google Scholar
  29. M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: https://doi.org/10.1006/inco.1994.1092.
  30. Y. Venema. A Modal Logic for Chopping Intervals. Journal of Logic and Computation, 1(4):453-476, 1991. URL: https://doi.org/10.1093/logcom/1.4.453.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact