Abstract
The logic of Bunched implications (BI) and its variants or extensions provide a powerful framework to deal with resources having static properties. In this paper, we propose a modal extension of BI logic, called DBI, which allows us to deal with dynamic resource properties. After defining a Kripke semantics for DBI, we illustrate the interest of DBI for expressing some dynamic properties and then we propose a labelled tableaux calculus for this logic. This calculus is proved sound and complete w.r.t. the Kripke semantics. Moreover, we also give a method for countermodel generation in this logic.
This work is supported by the ANR grant DynRes on Dynamic Resources and Separation and Update Logics (project no. ANR-11-BS02-011).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biri, N., Galmiche, D.: A Separation Logic for Resource Distribution. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 23–37. Springer, Heidelberg (2003)
Engberg, U., Winskel, G.: Completeness results for Linear Logic on Petri nets. Annals of Pure and Applied Logic 86, 101–135 (1997)
Galmiche, D., Méry, D.: Tableaux and Resource Graphs for Separation Logic. Journal of Logic and Computation 20(1), 189–231 (2010)
Galmiche, D., Méry, D., Pym, D.: The semantics of BI and Resource Tableaux. Math. Struct. in Comp. Science 15(6), 1033–1088 (2005)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: 28th ACM Symposium on Principles of Programming Languages, POPL 2001, London, UK, pp. 14–26 (2001)
Larchey-Wendling, D.: The Formal Proof of the Strong Completeness of Boolean BI (2012), http://www.loria.fr/~larchey/BBI
Larchey-Wendling, D., Galmiche, D.: The Undecidability of Boolean BI through Phase Semantics. In: 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, Edinburgh, UK, pp. 147–156 (July 2010)
Milner, R.: Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)
O’Hearn, P.W., Pym, D.J.: The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Pym, D.J., Tofts, C.: Systems modelling via resources and processes: Philosophy, calculus, semantics, and logic. Electronic Notes in Theoretical Computer Science 172, 545–587 (2007)
Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers (2002)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science, Copenhagen, Danemark, pp. 55–74 (July 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Courtault, J.R., Galmiche, D. (2013). A Modal BI Logic for Dynamic Resource Properties. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2013. Lecture Notes in Computer Science, vol 7734. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35722-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-35722-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35721-3
Online ISBN: 978-3-642-35722-0
eBook Packages: Computer ScienceComputer Science (R0)