A Simple Separation Logic

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 v1 and v2 . 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 v1 and truth of ϕ2 in all total extensions of v2 ; and second, as truth of ϕ1 in some total extension of v1 and truth of ϕ2 in some total extension of v2 . 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.