Semipositivity in Separation Logic with Two Variables

  • Zhilin WuEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


In a recent work by Demri and Deters (CSL-LICS 2014), first-order separation logic restricted to two variables and separating implication was shown undecidable, where it was shown that even with only two variables, if the use of negations is unrestricted, then they can be nested with separating implication in a complex way to get the undecidability result. In this paper, we revisit the decidability and complexity issues of first-order separation logic with two variables, and proposes semi-positive separation logic with two-variables (SPSL2), where the use of negations is restricted in the sense that negations can only occur in front of atomic formulae. We prove that satisfiability of the fragment of SPSL2 where neither separating conjunction nor septraction (the dual operator of separating implication) occurs in the scope of universal quantifiers, is \(\textsc {nexptime}\)-complete. As a byproduct of the proof, we show that the finite satisfiability problem of first-order logic with two variables and a bounded number of function symbols is \(\textsc {nexptime}\)-complete (the lower bound holds even with only one function symbol and without unary predicates), which may be of independent interest beyond separation logic community.


Function Symbol Partial Function Atomic Formula Universal Quantifier Dual Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



This work was partially done when I was a visiting researcher at LIAFA, Université Paris Diderot, from June 2014 to June 2015, supported by China Scholarship Council. My great thanks go to Stéphane Demri for the numerous discussions with him when I did this work. At last, I would like to thank the reviewers for their valuable comments.


  1. 1.
    Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411–425. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54830-7_27 CrossRefGoogle Scholar
  2. 2.
    Benaim, S., Benedikt, M., Charatonik, W., Kieroński, E., Lenhardt, R., Mazowiecki, F., Worrell, J.: Complexity of two-variable logic on finite trees. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 74–88. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39212-2_10 Google Scholar
  3. 3.
    Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Logic 12(4), 27 (2011)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106–137 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001). doi: 10.1007/3-540-45294-X_10 CrossRefGoogle Scholar
  6. 6.
    Charatonik, W., Kieroński, E., Mazowiecki, F.: Decidability of weak logics with deterministic transitive closure. In: CSL-LICS (2014)Google Scholar
  7. 7.
    Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235–249. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-23217-6_16 CrossRefGoogle Scholar
  8. 8.
    Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. In: CSL-LICS, pp. 1–37 (2014)Google Scholar
  9. 9.
    Demri, S., Deters, M.: Two-variable separation logic and its inner circle. ACM Trans. Comput. Logic 16(2), 15 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Demri, S., Galmiche, D., Larchey-Wendling, D., Méry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125–138. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06686-8_10 Google Scholar
  11. 11.
    Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Grädel, E., Otto, M.: On logics with two variables. Theor. Comput. Sci. 224(1–2), 73–113 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: LICS, pp. 306–317 (1997)Google Scholar
  14. 14.
    Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Arch. Math. Log. 38(4–5), 313–354 (1999)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Upper Saddle River (1967)zbMATHGoogle Scholar
  16. 16.
    Pacholski, L., aw Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. Comput. 29(4), 1083–1117 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_54 CrossRefGoogle Scholar
  18. 18.
    Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. J. Logic Lang. Inf. 14(3), 369–395 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Pratt-Hartmann, I.: The two-variable fragment with counting revisited. In: Dawar, A., Queiroz, R. (eds.) WoLLIC 2010. LNCS (LNAI), vol. 6188, pp. 42–54. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-13824-9_4 CrossRefGoogle Scholar
  20. 20.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)Google Scholar
  21. 21.
    Segoufin, L., ten Cate, B.: Unary negation. LMCS 9(3), 1–46 (2013)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Thakur, A., Breck, J., Reps, Th.: Satisfiability modulo abstraction for separation logic with linked lists. In: SPIN, pp. 58–67 (2014)Google Scholar
  23. 23.
    Trakhtenbrot, B.: Impossibility of an algorithm for the decision problem in finite classes. AMS Translations Ser. 2(23), 1–5 (1963)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingPeople’s Republic of China

Personalised recommendations