# A Simple Separation Logic

Herzig, Andreas A Simple Separation Logic. (2013) In: International Workshop Logic, Language, Information, and Computation - WoLLIC 2013, 20 August 2013 - 23 August 2013 (Darmstadt, Germany).

 Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
233kB

Official URL: http://dx.doi.org/10.1007/978-3-642-39992-3_16

## 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.

Item Type: Conference or Workshop Item (Paper) Thanks to IEEE editor. The definitive version is available at http://link.springer.com/chapter/10.1007%2F978-3-642-39992-3_16 hal-01147307 International conference proceedings Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) download 14 Apr 2015 13:40

Repository Staff Only: item control page