research-article

Nondeterministic Phase Semantics and the Undecidability of Boolean BI

Authors:

Dominique Larchey-Wendling,

Didier GalmicheAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 14, Issue 1

Article No.: 6, Pages 1 - 41

https://doi.org/10.1145/2422085.2422091

Published: 01 February 2013 Publication History

Abstract

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered the core of separation and spatial logics. For this, we define a complete phase semantics suitable for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out the elementary fragment of ILL, which is both undecidable and complete for trivial phase semantics. Thus, we obtain the undecidability of BBI.

References

[1]

Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR’97). Lecture Notes in Computer Science, vol. 1243. Springer, Berlin, 135--150.

Digital Library

[2]

Brotherston, J. 2010. A unified display proof theory for bunched logic. Electr. Notes Theor. Comput. Sci. 265, 197--211.

Digital Library

[3]

Brotherston, J. and Calcagno, C. 2009. Classical BI: A logic for reasoning about dualising resources. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 328--339.

Digital Library

[4]

Brotherston, J. and Kanovich, M. I. 2010. Undecidability of propositional separation logic and its neighbours. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science. 130--139.

Digital Library

[5]

Calcagno, C., Cardelli, L., and Gordon, A. 2005. Deciding validity in a spatial logic for trees. J. Func. Program. 15, 4, 543--572.

Digital Library

[6]

Calcagno, C., O’Hearn, P. W., and Yang, H. 2007. Local action and abstract separation logic. In Proceedings of the 22nd IEEE Symposium on Logic in Computer Science. 366--378.

Digital Library

[7]

de Groote, P., Guillaume, B., and Salvati, S. 2004. Vector addition tree automata. In Proceedings of the 19th IEEE Symposium on Logic in Computer Science. 64--73.

Digital Library

[8]

Galmiche, D. and Larchey-Wendling, D. 2006. Expressivity properties of Boolean BI through relational models. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06). Lecture Notes in Computer Science, vol. 4337. Springer, Berlin, 357--368.

Digital Library

[9]

Galmiche, D., Méry, D., and Pym, D. 2005. The semantics of BI and resource tableaux. Math. Struct. Comput. Sci. 15, 6, 1033--1088.

Digital Library

[10]

Ghilardi, S. and Meloni, G. 1990. Modal logics with n-ary connectives. Zeitschr. f. math. Logik und Grundlagen d. Math 36, 193--215.

[11]

Girard, J.-Y. 1987. Linear logic. Theor. Comput. Sci. 50, 1, 1--102.

Digital Library

[12]

Ishtiaq, S. and O’Hearn, P. 2001. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 14--26.

Digital Library

[13]

Kanovich, M. 1994. Linear logic as a logic of computations. Ann. Pure Appl. Logic 67, 1--3, 183--212.

[14]

Kanovich, M. 1995. The direct simulation of Minsky machines in linear logic. In Advances in Linear Logic, J.-Y. Girard, Y. Lafont, and L. Regnier Eds., London Mathematical Society Lecture Notes, vol. 222. Cambridge University Press, Chapter 2, 123--145.

Digital Library

[15]

Lafont, Y. 1996. The undecidability of second order linear logic without exponentials. J. Symbolic Logic 61, 2, 541--548.

[16]

Lafont, Y. and Scedrov, A. 1996. The undecidability of second order multiplicative linear logic. Inf. Comput. 125, 1, 46--51.

Digital Library

[17]

Larchey-Wendling, D. 2010. An alternative direct simulation of minsky machines into classical bunched logics via group semantics. Electr. Notes Theor. Comput. Sci. 265, 369--387.

Digital Library

[18]

Larchey-Wendling, D. and Galmiche, D. 2009. Exploring the relation between Intuitionistic BI and Boolean BI: An unexpected embedding. Math. Struct. Comput. Sci. 19, 3, 435--500.

Digital Library

[19]

Larchey-Wendling, D. and Galmiche, D. 2010. The undecidability of Boolean BI through phase semantics. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science. 140--149.

Digital Library

[20]

Martí-Oliet, N. and Meseguer, J. 1991. From Petri nets to linear logic. Math. Struct. Comput. Sci. 1, 1, 69--101.

[21]

Minsky, M. 1961. Recursive unsolvability of Post’s problem of ‘tag’ and other topics in the theory of Turing machines. Ann. Math. 74, 3, 437--455.

[22]

O’Hearn, P. and Pym, D. 1999. The logic of bunched implications. Bull. Symbolic Logic 5, 2, 215--244.

[23]

Okada, M. 2002. A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theor. Comput. Sci. 281, 1--2, 471--498.

[24]

Pym, D. 2002. The semantics and proof theory of the logic of bunched implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers. Errata available at http://www.cs.ac.uk/~pym/pym-tofts-fac-errata.pdf.

[25]

Reisig, W. 1985. Petri nets, an introduction. EATCS, Monographs on Theoretical Computer Science, Springer Verlag, Berlin.

Digital Library

[26]

Troelstra, A. 1992. Lectures on linear logic. Lecture Notes Series, vol. 29. CSLI, Stanford, CA.

[27]

Yetter, D. 1990. Quantales and (noncommutative) linear logic. J. Symbolic Logic 55, 1, 41--64.

Cited By

van Ditmarsch HGalmiche DGawek M(2023)An Epistemic Separation Logic with Action ModelsJournal of Logic, Language and Information10.1007/s10849-022-09372-z32:1(89-116)Online publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1007/s10849-022-09372-z
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Forster YLarchey-Wendling DMahboubi AMyreen M(2019)Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machinesProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294096(104-117)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294096
Show More Cited By

Index Terms

Nondeterministic Phase Semantics and the Undecidability of Boolean BI
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
    1. Finite Model Theory
    2. Proof theory
  2. Models of computation
    1. Computability

Recommendations

The Undecidability of Boolean BI through Phase Semantics
LICS '10: Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the core of separation and spatial logics. For this, we define a complete phase semantics for BBI and characterize it as trivial phase semantics. We ...
The decidability of the intensional fragment of classical linear logic

Intensional classical linear logic (MELL) is proved decidable.Intensional interlinear logic (RLL) is proved decidable.We adapt Kripke's method used to prove decidability for some relevance logics.The semi-relevant RLL emerges as a logic superior to MELL ...
A theorem prover for Boolean BI
POPL '13

While separation logic is acknowledged as an enabling technology for large-scale program verification, most of the existing verification tools use only a fragment of separation logic that excludes separating implication. As the first step towards a ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 14, Issue 1

February 2013

263 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2422085

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 February 2013

Accepted: 01 February 2012

Revised: 01 October 2011

Received: 01 May 2011

Published in TOCL Volume 14, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Agence Nationale de la Recherche
University Henri Poincaré of Nancy
Centre National de la Recherche Scientifique

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)2

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

van Ditmarsch HGalmiche DGawek M(2023)An Epistemic Separation Logic with Action ModelsJournal of Logic, Language and Information10.1007/s10849-022-09372-z32:1(89-116)Online publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1007/s10849-022-09372-z
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Forster YLarchey-Wendling DMahboubi AMyreen M(2019)Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machinesProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294096(104-117)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294096
Demri SFervari R(2019)The power of modal separation logicsJournal of Logic and Computation10.1093/logcom/exz019Online publication date: 19-Dec-2019
https://doi.org/10.1093/logcom/exz019
Hóu ZSanán DTiu ALiu Y(2017)Proof Tactics for Assertions in Separation LogicInteractive Theorem Proving10.1007/978-3-319-66107-0_19(285-303)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_19
Demri SDeters M(2016)Expressive Completeness of Separation Logic with Two Variables and No Separating ConjunctionACM Transactions on Computational Logic10.1145/283549017:2(1-44)Online publication date: 7-Jan-2016
https://dl.acm.org/doi/10.1145/2835490
Lazić RSchmitz S(2015)Nonelementary Complexities for Branching VASS, MELL, and ExtensionsACM Transactions on Computational Logic10.1145/273337516:3(1-30)Online publication date: 2-Jun-2015
https://dl.acm.org/doi/10.1145/2733375
Demri SDeters M(2015)Two-Variable Separation Logic and Its Inner CircleACM Transactions on Computational Logic10.1145/272471116:2(1-36)Online publication date: 21-Apr-2015
https://dl.acm.org/doi/10.1145/2724711
Hóu ZGoré RTiu A(2015)A labelled sequent calculus for BBI: proof theory and proof searchJournal of Logic and Computation10.1093/logcom/exv03328:4(809-872)Online publication date: 9-Jun-2015
https://doi.org/10.1093/logcom/exv033
Demri SDeters M(2015)Separation logics and modalities: a surveyJournal of Applied Non-Classical Logics10.1080/11663081.2015.101880125:1(50-99)Online publication date: Apr-2015
https://doi.org/10.1080/11663081.2015.1018801
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents