Document Open Access Logo

A Quantitative Extension of Interval Temporal Logic over Infinite Words

Authors Laura Bozzelli, Adriano Peron

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.11.pdf
  • Filesize: 0.81 MB
  • 16 pages

Document Identifiers

Author Details

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

Cite As Get BibTex

Laura Bozzelli and Adriano Peron. A Quantitative Extension of Interval Temporal Logic over Infinite Words. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TIME.2022.11

Abstract

Model checking (MC) for Halpern and Shoham’s interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHS_{simple} of DHS proving in addition that the considered problems for this fragment are at least 2Expspace-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHS_{simple}, the problems are Expspace-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Interval temporal logic
  • Homogeneity Assumption
  • Quantitative Constraints
  • Model checking
  • Decision Procedures
  • Complexity issues
  • Linear-time Hybrid Logics

Metrics

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

Related Versions

References

  1. J.F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. URL: https://doi.org/doi/10.1145/182.358434.
  2. L. Bozzelli and R. Lanotte. Complexity and succinctness issues for linear-time hybrid logics. Theor. Comput. Sci., 411(2):454-469, 2010. URL: https://doi.org/10.1016/j.tcs.2009.08.009.
  3. L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. Model checking interval temporal logics with regular expressions. Information and Computation, 272:104498, 2020. URL: https://doi.org/10.1016/j.ic.2019.104498.
  4. 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. URL: https://doi.org/10.1007/978-3-319-40229-1_27.
  5. 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. Information and Computation, 262(Part):241-264, 2018. URL: https://doi.org/10.1016/j.ic.2018.09.006.
  6. 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://doi.org/10.1145/3281028.
  7. 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.
  8. 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. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/lmcs-18(1:24)2022.
  9. L. Bozzelli, A. Montanari, and A. Peron. Complexity analysis of a unifying algorithm for model checking interval temporal logic. Inf. Comput., 280:104640, 2021. URL: https://doi.org/10.1016/j.ic.2020.104640.
  10. L. Bozzelli, A. Montanari, A. Peron, and P. Sala. Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete. In Proc. 12th GandALF, EPTCS 346, pages 179-194, 2021. URL: https://doi.org/10.4204/EPTCS.346.12.
  11. L. Bozzelli, A. Montanari, A. Peron, and P. Sala. Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes. In Proc. 28th TIME, LIPIcs 206, pages 9:1-9:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.TIME.2021.9.
  12. L. Bozzelli and A. Peron. A quantitative extension of interval temporal logic over infinite words. CoRR, abs/2206.13920, 2022. URL: http://arxiv.org/abs/2206.13920.
  13. 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.
  14. S. Demri, R. Lazic, and A. Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci., 411(22-24):2298-2316, 2010. URL: https://doi.org/10.1016/j.tcs.2010.02.021.
  15. 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.
  16. M. Franceschet, M. de Rijke, and B.H. Schlingloff. Hybrid Logics on Linear Structures: Expressivity and Complexity. In Proc. 10th TIME-ICTL, pages 166-173. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/TIME.2003.1214893.
  17. J.Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM, 38(4):935-962, 1991. URL: https://doi.org/10.1145/115234.115351.
  18. D. Harel. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM, 33(1):224-248, 1986. URL: https://doi.org/10.1145/4904.4993.
  19. J.A.W. Kamp. Tense logic and the theory of linear order. University of California, Los Angeles, 1968. Google Scholar
  20. R. Koymans. Specifying real-time properties with metric temporal logic. Real Time Syst., 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  21. O. Kupferman, N. Piterman, and M.Y. Vardi. Extended temporal logic revisited. In Proc. 12th CONCUR, LNCS 2154, pages 519-535. Springer, 2001. URL: https://doi.org/10.1007/3-540-44685-0_35.
  22. 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.
  23. A. Lomuscio and J. Michaliszyn. An epistemic Halpern-Shoham logic. In Proc. 23rd IJCAI, pages 1010-1016. IJCAI/AAAI, 2013. Google Scholar
  24. 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. IOS Press, 2014. URL: https://doi.org/10.3233/978-1-61499-419-0-543.
  25. 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.
  26. J. Marcinkowski and J. Michaliszyn. The undecidability of the logic of subintervals. Fundamenta Informaticae, 131(2):217-240, 2014. URL: https://doi.org/10.3233/FI-2014-1011.
  27. 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.
  28. A. Molinari, A. Montanari, and A. Peron. Model checking for fragments of Halpern and Shoham’s interval temporal logic based on track representatives. Information and Computation, 259(3):412-443, 2018. URL: https://doi.org/10.1016/j.ic.2017.08.011.
  29. B. Moszkowski. Reasoning About Digital Circuits. PhD thesis, Dept. of Computer Science, Stanford University, Stanford, CA, 1983. Google Scholar
  30. A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  31. P. Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. Google Scholar
  32. T. Schwentick and V. Weber. Bounded-Variable Fragments of Hybrid Logics. In Proc. 24th STACS, volume 4393 of LNCS 4393, pages 561-572. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-70918-3_48.
  33. M.Y. Vardi. Reasoning about the past with two-way automata. In Proc. 25th ICALP, LNCS 1443, pages 628-641. Springer, 1998. URL: https://doi.org/10.1007/BFb0055090.
  34. Y. Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. URL: https://doi.org/10.1305/ndjfl/1093635589.
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 About DROPS Imprint Privacy Contact