Document Open Access Logo

Interval Temporal Logic for Visibly Pushdown Systems

Authors Laura Bozzelli, Angelo Montanari, Adriano Peron

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2019.33.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Subject Classification

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

Metrics

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

Abstract

In this paper, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures. Both homogeneity and visibility are assumed. The proposed logic, called nested BHS, supports branching-time both in the past and in the future, and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [R. Alur et al., 2004] and NWTL [R. Alur et al., 2007]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS. The proof exploits a non-trivial automata-theoretic construction.

Cite As Get BibTex

Laura Bozzelli, Angelo Montanari, and Adriano Peron. Interval Temporal Logic for Visibly Pushdown Systems. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 33:1-33:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.33

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

References

  1. J. F. Allen. Maintaining Knowledge about Temporal Intervals. Communications of the ACM, 26(11):832-843, 1983. Google Scholar
  2. R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman, and L. Libkin. First-Order and Temporal Logics for Nested Words. In Proc. 22nd LICS, pages 151-160. IEEE Computer Society, 2007. Google Scholar
  3. R. Alur, S. Chaudhuri, and P. Madhusudan. A fixpoint calculus for local and global program flows. In Proc. 33rd POPL, pages 153-165. ACM, 2006. Google Scholar
  4. R. Alur, K. Etessami, and P. Madhusudan. A Temporal Logic of Nested Calls and Returns. In Proc. 10th TACAS, volume 2988 of LNCS, pages 467-481. Springer, 2004. Google Scholar
  5. R. Alur and P. Madhusudan. Visibly Pushdown Languages. In Proc. 36th STOC, pages 202-211. ACM, 2004. Google Scholar
  6. R. Alur and P. Madhusudan. Adding nesting structure to words. Journal of ACM, 56(3):16:1-16:43, 2009. Google Scholar
  7. C. Baier and J.P. Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  8. L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. An in-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions. In Proc. 15th SEFM, LNCS 10469, pages 104-119. Springer, 2017. Google Scholar
  9. 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
  10. 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
  11. L. Bozzelli and C. Sánchez. Visibly Linear Temporal Logic. J. Autom. Reasoning, 60(2):177-220, 2018. Google Scholar
  12. D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity. Theor. Comput. Sci., 560:269-291, 2014. Google Scholar
  13. D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Decidability and Complexity of the Fragments of the Modal Logic of Allen’s Relations over the Rationals. Information and Computation, accepted for publication on February 20, 2019. Google Scholar
  14. K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, and J. Palsberg. Stack Size Analysis for Interrupt-Driven Programs. In Proc. 10th SAS, LNCS 2694, pages 109-126. Springer, 2003. Google Scholar
  15. T. Chen, F. Song, and Z. Wu. Global Model Checking on Pushdown Multi-Agent Systems. In Proc. 30th AAAI, pages 2459-2465. AAAI Press, 2016. Google Scholar
  16. 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
  17. J. Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM, 38(4):935-962, 1991. Google Scholar
  18. A. Lomuscio and J. Michaliszyn. An Epistemic Halpern-Shoham Logic. In Proc. 23rd IJCAI, pages 1010-1016, 2013. Google Scholar
  19. 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
  20. 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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  23. 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
  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. Google Scholar
  26. I. Pratt-Hartmann. Temporal propositions and their logic. Artificial Intelligence, 166(1-2):1-36, 2005. Google Scholar
  27. L. J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, MIT, 1974. Google Scholar
  28. Y. Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. Google Scholar
  29. I. Walukiewicz. Pushdown Processes: Games and Model Checking. In Proc. 8th CAV, pages 62-74, 1996. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact