Stéphane Demri
Abstract
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 smallest fragments of separation logic known to be undecidable, and this contrasts with the decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with nonelementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional interval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely related logics.
- J. Allen. 1983. Maintaining knowledge about temporal intervals. Communications of the ACM 26, 11 (1983), 832--843. Google Scholar
Digital Library
- K. Bansal, R. Brochenin, and E. Lozes. 2009. Beyond shapes: Lists with ordered data. In FOSSACS’09 (Lecture Notes in Computer Science), Vol. 5504. Springer, 425--439. Google ScholarDigital Library
- S. Benaim, M. Benedikt, W. Charatonik, E. Kieroński, R. Lenhardt, F. Mazowiecki, and J. Worrell. 2013. Complexity of two-variable logic over finite trees. In ICALP’13 (Lecture Notes in Computer Science), Vol. 7966. Springer, 74--88. Google ScholarDigital Library
- P. Blackburn, M. de Rijke, and Y. Venema. 2001. Modal Logic. Cambridge University Press. Google ScholarDigital Library
- M. Bojańczyk, C. David, A. Muscholl, Th. Schwentick, and L. Segoufin. 2011. Two-variable logic on data words. ACM Transactions on Computational Logic 12, 4 (2011), 27. Google ScholarDigital Library
- E. Börger, E. Grädel, and Y. Gurevich. 1997. The Classical Decision Problem. Springer.Google Scholar
- P. Bouyer. 2002. A logical characterization of data languages. Informational Processing Letters 84, 2 (2002), 75--85. Google ScholarDigital Library
- R. Brochenin, S. Demri, and E. Lozes. 2012. On the almighty wand. Information and Computation 211 (2012), 106--137. Google ScholarDigital Library
- J. Brotherston, C. Fuhs, N. Gorogiannis, and J. Navarro Perez. 2014. A decision procedure for satisfiability in separation logic with inductive predicates. In CSL-LICS’14. ACM. Google ScholarDigital Library
- J. Brotherston and M. Kanovich. 2014. Undecidability of propositional separation logic and its neighbours. Journal of the Association for Computing Machinery 61, 2 (2014). Google ScholarDigital Library
- C. Calcagno, P. O’Hearn, and H. Yang. 2001. Computability and complexity results for a spatial assertion language for data structures. In FSTTCS’01 (Lecture Notes in Computer Science), Vol. 2245. Springer, 108--119. Google ScholarDigital Library
- W. Charatonik, E. Kieroński, and F. Mazowiecki. 2014. Decidability of weak logics with deterministic transitive closure. In CSL-LICS’14. ACM. Google ScholarDigital Library
- B. Cook, Ch. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. 2011. Tractable reasoning in a fragment of separation logic. In CONCUR’11 (Lecture Notes in Computer Science). Springer, 235--249. Google ScholarDigital Library
- J.-R. Courtault and D. Galmiche. 2013. A modal BI logic for dynamic resource properties. In LFCS’13 (Lecture Notes in Computer Science), Vol. 7734. Springer, 134--148.Google Scholar
- C. David. 2009. Analyse de XML avec données non-bornées. Ph.D. Dissertation. LIAFA, Université Paris VII.Google Scholar
- A. Dawar, Ph. Gardner, and G. Ghelli. 2007. Expressiveness and complexity of graph logic. Information and Computation 205, 3 (2007), 263--310. Google ScholarDigital Library
- M. de Rijke. 1992. The modal logic of inequality. Journal of Symbolic Logic 57, 2 (1992), 566--584.Google ScholarCross Ref
- N. Decker, P. Habermehl, M. Leucker, and D. Thoma. 2014. Ordered navigation on multi-attributed data words. In CONCUR’14 (Lecture Notes in Computer Science), Vol. 8704. 497--511.Google Scholar
- A. Degtyarev, M. Fisher, and A. Lisitsa. 2002. Equality and monodic first-order temporal logic. Studia Logica 72, 2 (2002), 147--156.Google ScholarCross Ref
- S. Demri and M. Deters. 2014. Expressive completeness of separation logic with two variables and no separating conjunction. In CSL-LICS’14. ACM, 37. Google ScholarDigital Library
- S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. 2014. Separation logic with one quantified variable. In CSR’14 (Lecture Notes in Computer Science), Vol. 8476. Springer, 125--138.Google Scholar
- S. Demri and Ph. Schnoebelen. 2002. The complexity of propositional linear temporal logics in simple cases. Information and Computation 174, 1 (2002), 84--103. Google ScholarDigital Library
- K. Etessami, M. Vardi, and Th. Wilke. 1997. First-order logic with two variables and unary temporal logics. In LICS’97. IEEE, 228--235. Google ScholarDigital Library
- D. Figueira. 2010. Reasoning on Words and Trees with Data. Ph.D. Dissertation. ENS de Cachan.Google Scholar
- D. Gabbay. 1981. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic. Reidel, 91--117.Google Scholar
- D. Gabbay and V. Shehtman. 1993. Undecidability of modal and intermediate first-order logics with two individual variables. Journal of Symbolic Logic 58, 3 (1993), 800--823.Google ScholarCross Ref
- E. Grädel, Ph. Kolaitis, and M. Vardi. 1997a. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic 3, 1 (1997), 53--69.Google ScholarCross Ref
- E. Grädel, M. Otto, and E. Rosen. 1997b. Two-variable logic with counting is decidable. In LICS’97. IEEE, 306--317. Google ScholarDigital Library
- E. Grädel, M. Otto, and E. Rosen. 1999. Undecidability results on two-variable logics. Archive for Mathematical Logic 38, 4--5 (1999), 313--354.Google Scholar
- J. Halpern. 1995. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence 75, 2 (1995), 361--372. Google ScholarDigital Library
- D. Harel, D. Kozen, and J. Tiuryn. 2000. Dynamic Logic. MIT Press. Google ScholarDigital Library
- M. Hennessy and R. Milner. 1980. On observing nondeterminism and concurrency. In ICALP’80 (Lecture Notes in Computer Science), Vol. 85. Springer, 299--309. Google ScholarDigital Library
- R. Iosif, A. Rogalewicz, and J. Simacek. 2013. The tree width of separation logic with recursive definitions. In CADE’13 (Lecture Notes in Computer Science), Vol. 7898. Springer, 21--38. Google ScholarDigital Library
- A. S. Kahr, E. F. Moore, and H. Wang. 1962. Entscheidungsproblem reduced to the ∀ ∃ ∀ case. Proceedings of the National Academy of Sciences of the USA. 48, 3 (1962), 365--377.Google ScholarCross Ref
- E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera. 2012. Two-variable first-order logic with equivalence closure. In LICS’12. IEEE, 431--440. Google ScholarDigital Library
- D. Larchey-Wendling and D. Galmiche. 2013. Nondeterministic phase semantics and the undecidability of boolean BI. ACM Transactions on Computational Logic 14, 1 (2013). Google ScholarDigital Library
- H. Lewis. 1980. Complexity results for classes of quantificational formulas. Journal of Computer System Sciences 21 (1980), 317--353.Google ScholarCross Ref
- C. Lutz and U. Sattler. 2002. The complexity of reasoning with Boolean modal logics. In Advances in Modal Logics 2000. Vol. 3. World Scientific, 329--348.Google Scholar
- M. L. Minsky. 1967. Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River, NJ. Google ScholarDigital Library
- Ch. Morgan. 1976. Methods for automated theorem proving in non classical logics. IEEE Transactions on Computers 25, 8 (1976), 852--862. Google ScholarDigital Library
- M. Mortimer. 1975. On language with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 21 (1975), 135--140.Google ScholarCross Ref
- B. Moszkowski. 1983. Reasoning About Digital Circuits. Technical Report STAN--CS--83--970. Dept. of Computer Science, Stanford University, Stanford, CA.Google Scholar
- B. Moszkowski. 2004. A hierarchical completeness proof for propositional interval temporal logic with finite time. Journal of Applied Non-Classical Logics 14, 1--2 (2004), 55--104.Google ScholarCross Ref
- M. Otto. 2001. Two variable first-order logic over ordered domains. Journal of Symbolic Logic 66, 2 (2001), 685--702.Google ScholarCross Ref
- L. Pacholski, W. Szwast, and L. Tendera. 1997. Complexity of two-variable logic with counting. In LICS’97. IEEE, 318--327. Google ScholarDigital Library
- A. Prior. 1967. Past, Present and Future. Oxford University Press.Google Scholar
- M. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Transactions on the American Mathematics Society 41 (1969), 1--35.Google Scholar
- J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS’02. IEEE, 55--74. Google ScholarDigital Library
- Th. Schwentick and Th. Zeume. 2012. Two-variable logic and two order relations. Logical Methods in Computer Science 8 (2012), 1--27.Google ScholarCross Ref
- D. Scott. 1962. A decision method for validity of sentences in two variables. Journal of Symbolic Logic 27 (1962), 377.Google Scholar
- L. Stockmeyer. 1974. The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. Dissertation. Department of Electrical Engineering, MIT.Google Scholar
- W. Szwast and L. Tendera. 2013. FO2 with one transitive relation is decidable. In STACS’13 (LIPIcs), Vol. 20. 317--328.Google Scholar
- J. van Benthem. 1976. Correspondence Theory. Ph.D. Dissertation. Mathematical Institute, University of Amsterdam.Google Scholar
- Ph. Weis. 2011. Expressiveness and Succinctness of First-Order Logic on Finite Words. Ph.D. Dissertation. University of Massachussetts. Google ScholarDigital Library
- H. Yang. 2001. Local Reasoning for Stateful Programs. Ph.D. Dissertation. University of Illinois, Urbana-Champaign. Google ScholarDigital Library
- Z. Chaochen. 2008. In Logics of Specification Languages, D. Bjorner and M. Henson (Eds.). Springer, Chapter Reviews on “Duration Calculus,” 609--611. Monographs in Theoretical Computer Science. An EATCS Series.Google Scholar
Index Terms
- Two-Variable Separation Logic and Its Inner Circle
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 ...
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 ...
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making ...
Reviews
Markus Wolf
Separation logic, an extension of Hoare logic, is currently a very active area of research. This paper investigates the expressiveness of this logic by exploring various restricted forms of it. Relations between fragments of separation logic and related logics are also studied, and via translations the relationships between these logics are expressed. The introduction of the paper explains known results, describes the results that are derived in the following sections, and gives a map showing the relationships between the various logics. The following sections introduce some restricted form of separation logic where formulas contain only one record field and a finite number of bounded variables. Next, some formulas often used in the following sections are defined and an encoding of data words via these formulas is presented. The kind of heaps used in this encoding, called fishbone heaps, are used a lot throughout the remainder of the paper. Finally, the section is concluded by the presentation of a new special variant modal logic for describing heaps. Section 3 builds on the previous section by further advancing the technical terms and constructing a translation from the propositional temporal interval logic into separation logic with two quantified variables and without the so-called "magic wand" operator. The possibility of this translation yields that separation logic with two quantified variables is decidable but not elementary recursive. The fourth section finally proves that the satisfiability problem of the separation logic with two bounded variables and the "magic wand" operator is not decidable. This is achieved by encoding Minsky machines and reducing the halting problem. A conclusion wraps up the results and points out some research directions. The paper contains a lot of technical tricks, which are nevertheless presented in a way that is very intuitively graspable. The intuition of fishbone heaps and the depiction of their structure are very helpful. On the whole, I consider this a very enjoyable paper. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments