Document Open Access Logo

Labelled Tableaux for Linear Time Bunched Implication Logic

Authors Didier Galmiche, Daniel Méry

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.31.pdf
  • Filesize: 0.74 MB
  • 17 pages

Document Identifiers

Author Details

Didier Galmiche
  • Université de Lorraine, CNRS, LORIA, Nancy, France
Daniel Méry
  • Université de Lorraine, CNRS, LORIA, Nancy, France

Funding

Work supported by the ANR NARCO Project (ANR Grant 21-CE48-0011).

Cite AsGet BibTex

Didier Galmiche and Daniel Méry. Labelled Tableaux for Linear Time Bunched Implication Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.31

Abstract

In this paper, we define the logic of Linear Temporal Bunched Implications (LTBI), a temporal extension of the Bunched Implications logic BI that deals with resource evolution over time, by combining the BI separation connectives and the LTL temporal connectives. We first present the syntax and semantics of LTBI and illustrate its expressiveness with a significant example. Then we introduce a tableau calculus with labels and constraints, called TLTBI, and prove its soundness w.r.t. the Kripke-style semantics of LTBI. Finally we discuss and analyze the issues that make the completeness of the calculus not trivial in the general case of unbounded timelines and explain how to solve the issues in the more restricted case of bounded timelines.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Temporal Logic
  • Bunched Implication Logic
  • Labelled Deduction
  • Tableaux

Metrics

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

References

  1. Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. The Journal of Logic and Algebraic Programming, 76(2):216-225, 2008. Google Scholar
  2. Edmund M Clarke and I Anca Draghicescu. Expressibility results for Linear-time and Branching-time Logics. In Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems), LNCS 354, pages 428-437. Springer, 1988. Google Scholar
  3. Jean-René Courtault and Didier Galmiche. A modal BI Logic for Dynamic Resource Properties. In Int. Symposium on Logical Foundations of Computer Science, LFCS 2013, LNCS 7734, pages 134-148. Springer, 2013. Google Scholar
  4. Jean-René Courtault and Didier Galmiche. A Modal Separation Logic for Resource Dynamics. Journal of Logic and Computation, 28(4):733-778, 2018. Google Scholar
  5. Didier Galmiche and Daniel Méry. Semantic Labelled Tableaux for Propositional BI without ⟂. Journal of Logic and Computation, 13(5):707-753, 2003. Google Scholar
  6. Didier Galmiche and Daniel Méry. Tableaux and Resource Graphs for Separation Logic. Journal of Logic and Computation, 20(1):189-231, 2010. Google Scholar
  7. Didier Galmiche, Daniel Méry, and David Pym. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science, 15(6):1033-1088, 2005. Google Scholar
  8. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. Google Scholar
  9. Samin S Ishtiaq and Peter W. O'Hearn. BI as an Assertion language for Mutable Data Structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 14-26, 2001. Google Scholar
  10. Norohiro Kamide. Temporal BI: proof system, semantics and translations. Theoretical Computer Science, 492:40-69, 2013. Google Scholar
  11. Fred Kröger and Stephan Merz. Temporal Logic and State Systems (Texts in Theoretical Computer Science. an EATCS Series). Springer Publishing Company, Incorporated, 2008. Google Scholar
  12. Dominique Larchey-Wendling and Didier Galmiche. The Undecidability of Boolean BI through phase Semantics. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 140-149. IEEE, 2010. Google Scholar
  13. Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  14. David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26. Applied Logic Series. Kluwer Academic Publishers, 2002. Google Scholar
  15. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pages 55-74, 2002. Google Scholar
  16. Kristin Y. Rozier. Linear Temporal Logic Symbolic Model Checking. Computer Science Review, 5(2):163-203, 2011. 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