Abstract
The kinds of models that are usually considered in separation logic are structures such as words, trees, and more generally pointer structures (heaps). In this paper we introduce the separation logic of much simpler structures, viz. sets. The models of our set separation logic are nothing but valuations of classical propositional logic. Separating a valuation V consists in splitting it up into two partial valuations v 1 and v 2. Truth of a formula φ 1 * φ 2 in a valuation V can then be defined in two different ways: first, as truth of φ 1 in all total extensions of v 1 and truth of φ 2 in all total extensions of v 2; and second, as truth of φ 1 in some total extension of v 1 and truth of φ 2 in some total extension of v 2. The first is an operator of separation of resources: the update of φ 1 * φ 2 by ψ is the conjunction of the update of φ 1 by ψ and the update of φ 2 by ψ; in other words, φ 1 * φ 2 can be updated independently. The second is an operator of separation of processes: updates by ψ 1 * ψ 2 can be performed independently. We show that the satisfiability problem of our logic is decidable in polynomial space (PSPACE). We do so by embedding it into dynamic logic of propositional assignments (which is PSPACE complete). We moreover investigate its applicability to belief update and belief revision, where the separation operators allow to formulate natural requirements on independent pieces of information.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alchourrón, C., Gärdenfors, P., Makinson, D.: On the logic of theory change: Partial meet contraction and revision functions. J. of Symbolic Logic 50, 510–530 (1985)
Balbiani, P., Herzig, A., Troquard, N.: Dynamic logic of propositional assignments: a well-behaved variant of PDL. In: Kupferman, O. (ed.) Logic in Computer Science (LICS), New Orleans, June 25-28. IEEE (2013), http://www.ieee.org/
Bienvenu, M., Herzig, A., Qi, G.: Prime implicate-based belief revision operators. In: Ghallab, M., Spyropoulos, C.D., Fakotakis, N., Avouris, N. (eds.) European Conference on Artificial Intelligence (ECAI), Patras, Greece, pp. 741–742. IOS Press (July 2008)
Brotherston, J., Kanovich, M.I.: Undecidability of propositional separation logic and its neighbours. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, Edinburgh, United Kingdom, July 11-14, pp. 130–139. IEEE Computer Society (2010)
van Ditmarsch, H., Herzig, A., de Lima, T.: From Situation Calculus to Dynamic Logic. Journal of Logic and Computation 21(2), 179–204 (2011), http://logcom.oxfordjournals.org/content/21/2/179.abstract?etoc
Gärdenfors, P.: Knowledge in Flux: Modeling the Dynamics of Epistemic States. MIT Press (1988)
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL, pp. 14–26. ACM (2001)
Katsuno, H., Mendelzon, A.O.: Propositional knowledge base revision and minimal change. Artificial Intelligence 52, 263–294 (1991)
Katsuno, H., Mendelzon, A.O.: On the difference between updating a knowledge base and revising it. In: Gärdenfors, P. (ed.) Belief Revision, pp. 183–203. Cambridge University Press (1992); Preliminary version in Allen, J.A., Fikes, R., Sandewall, E. (eds.) Principles of Knowledge Representation and Reasoning: Proc. 2nd Int. Conf., pp. 387–394. Morgan Kaufmann Publishers (1991)
Kourousias, G., Makinson, D.: Parallel interpolation, splitting, and relevance in belief change. Journal of Symbolic Logic 72(3), 994–1002 (2007)
Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean bi through phase semantics. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, Edinburgh, United Kingdom, July 11-14, pp. 140–149. IEEE Computer Society (2010)
McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Mitchie, D. (eds.) Machine Intelligence, vol. 4, pp. 463–502. Edinburgh University Press (1969)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Parikh, R.: Beliefs, belief revision, and splitting languages. In: Moss, L.S., Ginzburg, J., de Rijke, M. (eds.) Logic, Language, and Computation, vol. 2, pp. 266–278. CSLI Publications (1999)
Reiter, R.: The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 359–380. Academic Press, San Diego (1991)
Reiter, R.: Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, July 22-25, pp. 55–74. IEEE Computer Society (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herzig, A. (2013). A Simple Separation Logic. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2013. Lecture Notes in Computer Science, vol 8071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39992-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-39992-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39991-6
Online ISBN: 978-3-642-39992-3
eBook Packages: Computer ScienceComputer Science (R0)