Document Open Access Logo

Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic

Authors Laura Bozzelli, Angelo Montanari, Adriano Peron

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.18.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

Laura Bozzelli, Angelo Montanari, and Adriano Peron. Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.18

Abstract

The model-checking (MC) problem of Halpern and Shoham Interval Temporal Logic (HS) has been recently investigated in some papers and is known to be decidable. An intriguing open question concerns the exact complexity of the problem for full HS: it is at least EXPSPACE-hard, while the only known upper bound is non-elementary and is obtained by exploiting an abstract representation of Kripke structure paths called descriptors. In this paper we generalize the approach by providing a uniform framework for model-checking full HS and meaningful (almost maximal) fragments, where a specialized type of descriptor is defined for each fragment. We then devise a general MC alternating algorithm parameterized by the type of descriptor which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the time complexity of the algorithm and give, by non-trivial arguments, tight bounds on the length of certificates. For two types of descriptors, we obtain exponential upper and lower bounds which lead to an elementary MC algorithm for the related HS fragments. For the other types of descriptors, we provide non-elementary lower bounds. This last result addresses a question left open in some papers regarding the possibility of fixing an elementary upper bound on the size of the descriptors for full HS.

Subject Classification

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

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. Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments. In Proc. 8th IJCAR, LNAI 9706, pages 389-405. Springer, 2016. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison. ACM Trans. Comput. Logic, 20(1):4:1-4:31, 2019. Google Scholar
  6. 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. Google Scholar
  7. D. Bresolin, V. Goranko, A. Montanari, and P. Sala. Tableau-based decision procedures for the logics of subinterval structures over dense orderings. Journal of Logic and Computation, 20(1):133-166, 2010. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. J. Ferrante and C. Rackoff. A Decision Procedure for the First Order Theory of Real Addition with Order. SIAM Journal of Computation, 4(1):69-76, 1975. Google Scholar
  11. J. Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM, 38(4):935-962, 1991. Google Scholar
  12. K. Lodaya. Sharpening the Undecidability of Interval Temporal Logic. In Proc. 6th ASIAN, LNCS 1961, pages 290-298. Springer, 2000. Google Scholar
  13. A. Lomuscio and J. Michaliszyn. An Epistemic Halpern-Shoham Logic. In Proc. 23rd IJCAI, pages 1010-1016, 2013. Google Scholar
  14. A. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class of EHS specifications. In Proc. 21st ECAI, pages 543-548, 2014. Google Scholar
  15. J. Marcinkowski and J. Michaliszyn. The Undecidability of the Logic of Subintervals. Fundamenta Informaticae, 131(2):217-240, 2014. Google Scholar
  16. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. Acta Informatica, 53(6-8):587-619, 2016. Google Scholar
  17. A. Molinari, A. Montanari, and A. Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. In Proc. 24th CSL, pages 193-210, 2015. Google Scholar
  18. A. Molinari, A. Montanari, and A. Peron. Complexity of ITL model checking: some well-behaved fragments of the interval logic HS. In Proc. 22nd TIME, pages 90-100, 2015. Google Scholar
  19. Alberto Molinari, Angelo Montanari, and Adriano Peron. Model checking for fragments of Halpern and Shoham’s interval temporal logic based on track representatives. Inf. Comput., 259(3):412-443, 2018. Google Scholar
  20. A. Montanari, G. Puppis, and P. Sala. A decidable weakening of Compass Logic based on cone-shaped cardinal directions. Logical Methods in Computer Science, 11(4), 2015. Google Scholar
  21. B. Moszkowski. Reasoning About Digital Circuits. PhD thesis, Dept. of Computer Science, Stanford University, Stanford, CA, 1983. Google Scholar
  22. A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pages 46-57. IEEE, 1977. Google Scholar
  23. I. Pratt-Hartmann. Temporal propositions and their logic. Artificial Intelligence, 166(1-2):1-36, 2005. Google Scholar
  24. P. Roeper. Intervals and Tenses. Journal of Philosophical Logic, 9:451-469, 1980. Google Scholar
  25. Y. Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. Google Scholar
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