More Web Proxy on the site http://driver.im/

research-article

Expressive completeness of separation logic with two variables and no separating conjunction

Authors:

Stéphane Demri,

Morgan DetersAuthors Info & Claims

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Article No.: 37, Pages 1 - 10

https://doi.org/10.1145/2603088.2603142

Published: 14 July 2014 Publication History

Abstract

We show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak second-order logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these, and as a by-product identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction.

References

[1]

T. Antonopoulos and A. Dawar. Separating graph logic from MSO. In FOSSACS'09, volume 5504 of LNCS, pages 63--77. Springer, 2009.

Digital Library

[2]

T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In FOSSACS'14, volume 8412 of LNCS, pages 411--425. Springer, 2014.

[3]

E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.

[4]

M. Bozga, R. Iosif, and S. Perarnau. Quantitative separation logic and programs with lists. Journal of Automated Reasoning, 45(2):131--156, 2010.

Digital Library

[5]

D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric propositional neighborhood logics: Expressiveness, decidability, and undecidability. In ECAI'10, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 695--700. IOS Press.

Digital Library

[6]

R. Brochenin. Separation Logic: Expressiveness, Complexity, Temporal Extension. PhD thesis, LSV, ENS Cachan, September 2013.

[7]

R. Brochenin, S. Demri, and E. Lozes. On the Almighty Wand. Information and Computation, 211:106--137, 2012.

Digital Library

[8]

J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. In LICS'10, pages 130--139. IEEE.

Digital Library

[9]

C. Calcagno, P. O'Hearn, and H. Yang. Computability and complexity results for a spatial assertion language for data structures. In FSTTCS'01, volume 2245 of LNCS, pages 108--119. Springer, 2001.

Digital Library

[10]

B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR'11, volume 6901 of LNCS, pages 235--249. Springer, 2011.

Digital Library

[11]

A. Dawar, P. Gardner, and G. Ghelli. Expressiveness and complexity of graph logic. Information and Computation, 205(3):263--310, 2007.

Digital Library

[12]

S. Demri and M. Deters. Two-variable separation logic and its inner circle, September 2013. Under submission.

[13]

S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. Separation logic with one quantified variable. In CSR'14, volume 8476 of LNCS, pages 125--138. Springer, 2014.

[14]

K. Etessami, M. Vardi, and T. Wilke. First-order logic with two variables and unary temporal logics. In LICS'97, pages 228--235. IEEE, 1997.

Digital Library

[15]

D. Gabbay. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic, pages 91--117. Reidel, 1981.

[16]

D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic - Mathematical Foundations and Computational Aspects, Vol. 1. OUP, 1994.

Digital Library

[17]

D. Galmiche and D. Méry. Tableaux and resource graphs for separation logic. Journal of Logic and Computation, 20(1):189--231, 2010.

Digital Library

[18]

E. Grädel, M. Otto, and E. Rosen. Undecidability results on two-variable logics. Arch. Mathematical Logic, 38(4--5):313--354, 1999.

[19]

C. Haase, S. Ishtiaq, J. Ouaknine, and M. Parkinson. SeLoger: A tool for graph-based reasoning in separation logic. In CAV'13, volume 8044 of LNCS, pages 790--795. Springer, 2013.

Digital Library

[20]

Z. Hou, R. Clouston, R. Goré, and A. Tiu. Proof search for propositional abstract separation logics via labelled sequents. In POPL'14, pages 465--476. ACM, 2014.

Digital Library

[21]

N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In CSL'04, volume 3210 of LNCS, pages 160--174. Springer, 2004.

[22]

R. Iosif, A. Rogalewicz, and J. Simacek. The tree width of separation logic with recursive definitions. In CADE'13, volume 7898 of LNCS, pages 21--38. Springer, 2013.

Digital Library

[23]

V. Kuncak and M. Rinard. On spatial conjunction as second-order logic. Technical Report MIT--CSAIL--TR-2004-067, MIT CSAIL, October 2004.

[24]

D. Larchey-Wendling and D. Galmiche. The undecidability of Boolean BI through phase semantics. In LICS'10, pages 140--149. IEEE, 2010.

Digital Library

[25]

W. Lee and S. Park. A proof system for separation logic with magic wand. In POPL'14, pages 477--490. ACM, 2014.

Digital Library

[26]

C. Lutz, U. Sattler, and F. Wolter. Modal logic and the two-variable fragment. In CSL'01, volume 2142 of LNCS, pages 247--261. Springer.

Digital Library

[27]

R. Piskac, T. Wies, and D. Zufferey. Automating separation logic using SMT. In CAV'13, volume 8044 of LNCS, pages 773--789. Springer.

Digital Library

[28]

J. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55--74. IEEE, 2002.

Digital Library

[29]

B. Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. AMS Translations, Series 2, 23:1--5, 1963.

[30]

P. Weis. Expressiveness and Succinctness of First-Order Logic on Finite Words. PhD thesis, University of Massachussetts, 2011.

Digital Library

Cited By

Pagel JZuleger F(2022)Strong-separation LogicACM Transactions on Programming Languages and Systems10.1145/349884744:3(1-40)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3498847
Pagel JZuleger F(2021)Strong-Separation LogicProgramming Languages and Systems10.1007/978-3-030-72019-3_24(664-692)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_24
Echenim MIosif RPeltier N(2019)The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary DomainsFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_14(242-259)Online publication date: 5-Apr-2019
https://doi.org/10.1007/978-3-030-17127-8_14
Show More Cited By

Index Terms

Expressive completeness of separation logic with two variables and no separating conjunction
1. Theory of computation
  1. Logic
  2. Models of computation
    1. Computability

Recommendations

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction

Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, we show that first-order separation logic with one ...
Two-Variable Separation Logic and Its Inner Circle

Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the ...
Expressive completeness by separation for discrete time interval temporal logic with expanding modalities
Abstract
Recently we established an analog of Gabbay's separation theorem about linear temporal logic (LTL) for the extension of Moszkowski's discrete time propositional Interval Temporal Logic (ITL) by two sets of expanding modalities, namely the unary ...
Highlights
- Recently we established temporal separation for the extension of Moszkowski's discrete time ITL by the neighbourhood modalities.
- We show how temporal separation for ITL by the neighbourhood modalities facilitates a proof of this system'...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2014

764 pages

ISBN:9781450328869

DOI:10.1145/2603088

Program Chairs:
Thomas Henzinger
Institute of Science and Technology (IST), Austria
,
Dale Miller
INRIA and LIX/Ecole Polytechnique, Palaiseau

Copyright © 2014 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]

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

CSL-LICS '14

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC

July 14 - 18, 2014

Vienna, Austria

Acceptance Rates

CSL-LICS '14 Paper Acceptance Rate 74 of 212 submissions, 35%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
57
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pagel JZuleger F(2022)Strong-separation LogicACM Transactions on Programming Languages and Systems10.1145/349884744:3(1-40)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3498847
Pagel JZuleger F(2021)Strong-Separation LogicProgramming Languages and Systems10.1007/978-3-030-72019-3_24(664-692)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_24
Echenim MIosif RPeltier N(2019)The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary DomainsFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_14(242-259)Online publication date: 5-Apr-2019
https://doi.org/10.1007/978-3-030-17127-8_14
Demri SGalmiche DLarchey-Wendling DMéry D(2017)Separation Logic with One Quantified VariableTheory of Computing Systems10.1007/s00224-016-9713-161:2(371-461)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s00224-016-9713-1
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
Hóu ZTiu A(2016)Completeness for a First-Order Abstract Separation LogicProgramming Languages and Systems10.1007/978-3-319-47958-3_23(444-463)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_23
Wu Z(2016)Semipositivity in Separation Logic with Two VariablesDependable Software Engineering: Theories, Tools, and Applications10.1007/978-3-319-47677-3_12(179-196)Online publication date: 6-Oct-2016
https://doi.org/10.1007/978-3-319-47677-3_12
Gu XChen TWu Z(2016)A Complete Decision Procedure for Linearly Compositional Separation Logic with Data ConstraintsProceedings of the 8th International Joint Conference on Automated Reasoning - Volume 970610.1007/978-3-319-40229-1_36(532-549)Online publication date: 27-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-40229-1_36
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
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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents