Document Open Access Logo

Gabbay Separation for the Duration Calculus

Author Dimitar P. Guelev

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.10.pdf
  • Filesize: 0.72 MB
  • 14 pages

Document Identifiers

Author Details

Dimitar P. Guelev
  • Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria

Cite AsGet BibTex

Dimitar P. Guelev. Gabbay Separation for the Duration Calculus. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TIME.2022.10

Abstract

Gabbay’s separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In particular it enables a concise proof of Kamp’s seminal expressive completeness theorem for LTL. In 2000, Alexander Rabinovich established an expressive completeness result for a subset of the Duration Calculus (DC), a real-time interval temporal logic. DC is based on the chop binary modality, which restricts access to subintervals of the reference time interval, and is therefore regarded as introspective. The considered subset of DC is known as the ⌈P⌉-subset in the literature. Neighbourhood Logic (NL), a system closely related to {DC}, is based on the neighbourhood modalities, also written ⟨A⟩ and ⟨ ̄A⟩ in the notation stemming from Allen’s system of interval relations. These modalities are expanding as they allow writing future and past formulas to impose conditions outside the reference interval. This setting makes temporal separation relevant: is expressive power ultimately affected, if past constructs are not allowed in the scope of future ones, or vice versa? In this paper we establish an analogue of Gabbay’s separation theorem for the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities, and the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities and chop-based analogue of Kleene star. We show that the result applies if the weak chop inverses, a pair binary expanding modalities, are given the role of the neighbourhood modalities, by virtue of the inter-expressibility between them and the neighbourhood modalities in the presence of chop.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
Keywords
  • Gabbay separation
  • Neighbourhood Logic
  • Duration Calculus
  • expanding modalities

Metrics

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

References

  1. IEEE 1364-2005 - IEEE Standard for Verilog Hardware Description Language, 2005. URL: https://ieeexplore.ieee.org/document/1620780.
  2. IEEE 1850-2010 - IEEE Standard for Property Specification Language (PSL), 2010. URL: https://standards.ieee.org/standard/1850-2010.html.
  3. James F. Allen. Maintaining knowledge about temporal intervals. Commun. ACM, 26(11):832-843, 1983. URL: https://doi.org/10.1145/182.358434.
  4. Rana Barua, Suman Roy, and Zhou Chaochen. Completeness of neighbourhood logic. In Christoph Meinel and Sophie Tison, editors, STACS 99, Proceedings, volume 1563 of LNCS, pages 521-530. Springer, 1999. URL: https://doi.org/10.1007/3-540-49116-3_49.
  5. Marc Boulé and Zeljko Zilic. Psl and sva assertion languages. In Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring, pages 55-82. Springer Netherlands, Dordrecht, 2008. URL: https://doi.org/10.1007/978-1-4020-8586-4_4.
  6. Howard Bowman and Simon Thompson. A Decision Procedure and Complete Axiomatisation of Finite Interval Temporal Logic with Projection. Journal of Logic and Computation, 13(2):195-239, 2003. Google Scholar
  7. Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Interval vs. point temporal logic model checking: an expressiveness comparison. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, FSTTCS 2016, volume 65 of LIPIcs, pages 26:1-26:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.26.
  8. Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro 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.
  9. Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro 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.
  10. Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Alternating-time temporal logics with linear past. Theor. Comput. Sci., 813:199-217, 2020. URL: https://doi.org/10.1016/j.tcs.2019.11.028.
  11. Antonio Cau, Ben Moszkowski, and Hussein Zedan. ITL web pages. URL: http://www.antonio-cau.co.uk/ITL/. Google Scholar
  12. Michael Fisher. A normal form for temporal logics and its applications in theorem-proving and execution. J. Log. Comput., 7(4):429-456, 1997. URL: https://doi.org/10.1093/logcom/7.4.429.
  13. Dov Gabbay, Ian Hodkinson, and Mark Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects. Volume I. Oxford University Press, 1994. Google Scholar
  14. Dov M. Gabbay. Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In Proceedings of the Colloquium of Temporal Logic in Specification, volume 398 of LNCS, pages 67-89. Springer, 1989. Google Scholar
  15. Dimitar P. Guelev. A syntactical proof of the canonical reactivity form for past linear temporal logic. J. Log. Comput., 18(4):615-623, 2008. URL: https://doi.org/10.1093/logcom/exn002.
  16. Dimitar P. Guelev and Ben Moszkowski. A separation theorem for discrete-time interval temporal logic. Journal of Applied Non-Classical Logics, 32(1):28-54, 2022. URL: https://doi.org/10.1080/11663081.2022.2050135.
  17. François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal logic with forgettable past. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 383-392. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029846.
  18. François Laroussinie and Philippe Schnoebelen. A hierarchy of temporal logics with past (extended abstract). In Patrice Enjalbert, Ernst W. Mayr, and Klaus W. Wagner, editors, STACS 94, Proceedings, volume 775 of LNCS, pages 47-58. Springer, 1994. URL: https://doi.org/10.1007/3-540-57785-8_130.
  19. Zohar Manna and Amir Pnueli. A Hierarchy of Temporal Properties. In 9th Symposium on Principles of Distributed Computing, pages 377-408. ACM Press, 1990. Google Scholar
  20. Alberto Molinari, Angelo Montanari, Aniello Murano, Giuseppe Perelli, and Adriano Peron. Checking interval properties of computations. Acta Informatica, 53(6-8):587-619, 2016. URL: https://doi.org/10.1007/s00236-015-0250-1.
  21. Dario Della Monica, Angelo Montanari, and Pietro Sala. The importance of the past in interval temporal logics: The case of propositional neighborhood logic. In Alexander Artikis, Robert Craven, Nihan Kesim Cicekli, Babak Sadighi, and Kostas Stathis, editors, Logic Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the Occasion of His 60th Birthday, volume 7360 of LNCS, pages 79-102. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29414-3_6.
  22. Angelo Montanari, Aniello Murano, Giuseppe Perelli, and Adriano Peron. Checking interval properties of computations. In Amedeo Cesta, Carlo Combi, and François Laroussinie, editors, Proceedings of TIME 2014, pages 59-68. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/TIME.2014.24.
  23. Ben Moszkowski. Reasoning about Digital Circuits. Ph.D. thesis, Department of Computer Science, Stanford University, 1983. URL: http://www.antonio-cau.co.uk/ITL/publications/reports/thesis-ben.pdf.
  24. Ben Moszkowski. Temporal Logic For Multilevel Reasoning About Hardware. IEEE Computer, 18(2):10-19, 1985. Google Scholar
  25. Ben Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986. URL: http://www.antonio-cau.co.uk/ITL/publications/reports/tempura-book.pdf. Google Scholar
  26. Paritosh K. Pandya. Some extensions to propositional mean-value caculus: Expressiveness and decidability. In Hans Kleine Büning, editor, CSL '95, Selected Papers, volume 1092 of LNCS, pages 434-451. Springer, 1995. URL: https://doi.org/10.1007/3-540-61377-3_52.
  27. Paritosh K. Pandya. Model checking CTL*[DC]. In Tiziana Margaria and Wang Yi, editors, TACAS 2001, Proceedings, volume 2031 of LNCS, pages 559-573. Springer, 2001. URL: https://doi.org/10.1007/3-540-45319-9_38.
  28. Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium Foundations of Computer Science, pages 46-57. IEEE, 1977. Google Scholar
  29. Alexander Moshe Rabinovich. Expressive completeness of duration calculus. Inf. Comput., 156(1-2):320-344, 2000. URL: https://doi.org/10.1006/inco.1999.2816.
  30. Zhou Chaochen and Michael R. Hansen. Duration Calculus. A Formal Approach to Real-Time Systems. Springer, 2004. Google Scholar
  31. Zhou Chaochen, Michael R. Hansen, and Peter Sestoft. Decidability and undecidability results for duration calculus. In Patrice Enjalbert, Alain Finkel, and Klaus W. Wagner, editors, STACS 93, Proceedings, volume 665 of LNCS, pages 58-68. Springer, 1993. URL: https://doi.org/10.1007/3-540-56503-5_8.
  32. Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A Calculus of Durations. Information Processing Letters, 40(5):269-276, 1991. 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