Document Open Access Logo

Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison

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

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.26.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Laura Bozzelli
Alberto Molinari
Angelo Montanari
Adriano Peron
Pietro Sala

Cite AsGet BibTex

Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 26:1-26:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.26

Abstract

Model checking is a powerful method widely explored in formal verification to check the (state-transition) model of a system against desired properties of its behaviour. Classically, properties are expressed by formulas of a temporal logic, such as LTL, CTL, and CTL*. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. On the contrary, Halpern and Shoham's interval temporal logic (HS) is "interval-wise" interpreted, thus allowing one to naturally express properties of computation stretches, spanning a sequence of states, or properties involving temporal aggregations, which are inherently "interval-based". In this paper, we study the expressiveness of HS in model checking, in comparison with that of the standard logics LTL, CTL, and CTL*. To this end, we consider HS endowed with three semantic variants: the state-based semantics, introduced by Montanari et al., which allows branching in the past and in the future, the linear-past semantics, allowing branching only in the future, and the linear semantics, disallowing branching. These variants are compared, as for their expressiveness, among themselves and to standard temporal logics, getting a complete picture. In particular, HS with linear (resp., linear-past) semantics is proved to be equivalent to LTL (resp., finitary CTL*).
Keywords
  • Interval Temporal Logics
  • Expressiveness
  • 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. URL: http://dx.doi.org/10.1145/182.358434.
  2. R. Alur, P. Cerný, and S. Zdancewic. Preserving secrecy under refinement. In ICALP, LNCS 4052, pages 107-118, 2006. URL: http://dx.doi.org/10.1007/11787006_10.
  3. P. Blackburn and J. Seligman. What are hybrid languages? In AiML, pages 41-62, 1998. Google Scholar
  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 IJCAR, LNAI 9706, pages 389-405, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40229-1_27.
  5. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval vs. point temporal logic model checking: an expressiveness comparison. Technical report, Univ. of Udine, Italy, 2016. URL: http://www.uniud.it/it/ateneo-uniud/ateneo-uniud-organizzazione/dipartimenti/dima/ricerca/pubblicazioni/preprints/3.2016.
  6. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Model Checking the Logic of Allen’s Relations Meets and Started-by is 𝐏^NP-Complete. In GandALF, pages 76-90, 2016. URL: http://dx.doi.org/10.4204/EPTCS.226.6.
  7. 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: http://dx.doi.org/10.1007/s10472-013-9376-4.
  8. 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: http://dx.doi.org/10.1145/4904.4999.
  9. D. M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification, LNCS 398, pages 409-448, 1987. URL: http://dx.doi.org/10.1007/3-540-51803-7_36.
  10. J. Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935-962, 1991. URL: http://dx.doi.org/10.1145/115234.115351.
  11. H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Ucla, 1968. Google Scholar
  12. O. Kupferman, A. Pnueli, and M. Y. Vardi. Once and for all. J. Comput. Syst. Sci., 78(3):981-996, 2012. URL: http://dx.doi.org/10.1016/j.jcss.2011.08.006.
  13. K. Lodaya. Sharpening the undecidability of interval temporal logic. In ASIAN, LNCS 1961, pages 290-298, 2000. URL: http://dx.doi.org/10.1007/3-540-44464-5_21.
  14. A. Lomuscio and J. Michaliszyn. An epistemic Halpern-Shoham logic. In IJCAI, pages 1010-1016, 2013. Google Scholar
  15. A. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class of EHS specifications. In ECAI, pages 543-548, 2014. URL: http://dx.doi.org/10.3233/978-1-61499-419-0-543.
  16. A. Lomuscio and J. Michaliszyn. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In KR, pages 298-308, 2016. Google Scholar
  17. J. Marcinkowski and J. Michaliszyn. The undecidability of the logic of subintervals. Fundamenta Informaticae, 131(2):217-240, 2014. URL: http://dx.doi.org/10.3233/FI-2014-1011.
  18. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. Acta Informatica, 53(6):587-619, 2016. URL: http://dx.doi.org/10.1007/s00236-015-0250-1.
  19. A. Molinari, A. Montanari, and A. Peron. Complexity of ITL model checking: some well-behaved fragments of the interval logic HS. In TIME, pages 90-100, 2015. URL: http://dx.doi.org/10.1109/TIME.2015.12.
  20. A. Molinari, A. Montanari, and A. Peron. A model checking procedure for interval temporal logics based on track representatives. In CSL, pages 193-210, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.193.
  21. A. Molinari, A. Montanari, A. Peron, and P. Sala. Model Checking Well-Behaved Fragments of HS: the (Almost) Final Picture. In KR, pages 473-483, 2016. Google Scholar
  22. B. Moszkowski. Reasoning About Digital Circuits. PhD thesis, Stanford University, CA, USA, 1983. Google Scholar
  23. A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  24. I. Pratt-Hartmann. Temporal prepositions and their logic. Artificial Intelligence, 166(1-2):1-36, 2005. URL: http://dx.doi.org/10.1016/j.artint.2005.04.003.
  25. P. Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. Google Scholar
  26. M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for concurrency, pages 238-266. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-60915-6_6.
  27. Y. Venema. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. URL: http://dx.doi.org/10.1305/ndjfl/1093635589.
  28. T. Wilke. Classifying discrete temporal properties. In STACS, LNCS 1563, pages 32-46, 1999. URL: http://dx.doi.org/10.1007/3-540-49116-3_3.
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