Brotherston, J;
Kanovich, M;
(2014)
Undecidability of Propositional Separation Logic and Its Neighbours.
JOURNAL OF THE ACM
, 61
(2)
, Article ARTN 14. 10.1145/2542667.
![[thumbnail of a14-brotherston.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
a14-brotherston.pdf Download (1MB) |
Abstract
n this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language. The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models. Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained. In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI. Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete. All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
| Type: | Article |
|---|---|
| Title: | Undecidability of Propositional Separation Logic and Its Neighbours |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/2542667 |
| Publisher version: | http://dx.doi.org/10.1145/2542667 |
| Language: | English |
| Additional information: | Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the owner/author(s). Copyright is held by the author/owner(s). |
| Keywords: | Separation logic, undecidability, memory models, bunched logic |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1430439 |
Archive Staff Only
 |
View Item |
