-
1. Extended Abstract
In this talk we give an overview of researchs and results about so-called BI-based Separation Logics,
with a main focus on semantics and proofs. We present some key ideas, works and results mainly
developed in our research team in LORIA laboratory (Nancy, France) since more than twenty years.
After a reminder about resource models and resource logics we start by giving the BI logic (with
intuitionistic additives) [
1
], its bunched calculus (LBI) and its resource semantics that is complete only
for BI without ⊥ [
2
]. We also remind that BI logic, that focuses on resource separation and sharing,
is different from Linear Logic [
3
], that focuses instead on resource comsumption. We also consider
some variants of BI logic like Boolean BI (BBI) (with classical additives) [
4
] and BI’s Pointer logic, also
called Separation Logic (SL), that is based on BBI and deals with memory cells [
5
]. Separation Logic
has provided key developments in formal reasoning about programs with the frame rule that allows a
proof to be localized to the resources that a program component accesses andalso with the key notion
of local reasoning [
6, 7
]. We do not consider here the impressive developments from SL in the last
twenty years but we can mention the Concurrent Separation Logic [
8
], that allows modular reasoning
about threads that share storage and other resources, the Incorrectness Separation Logic [
9
], with
the goal of proving that compositional bug catchers find actual bugs and its concurrent extension to
account for bug catching in concurrent programs [
10
]. In the rest of the talk Separation logics denote
the (B)BI-based logics with separation and their extensions.
After this first part we introduce BI logic, its semantics and mainly on so-called resource tableaux, that
are labelled tableaux with resource constraints of two kinds (assertions and requirements), and also
define the key notion of resource graph [
2
]. The tableau calculus designed for BI logic is proved sound
and complete w.r.t. the Grothendick topological semantics (GR models). To solve the question to have
a semantics of BI based on partial monoids we propose different new semantics for BI logic, namely
a relational semantics (RM models), a Kripke resource semantics (KR models) and a partially defined
monoid semantics (PDM models) and show that the tableaux calculus is sound and complete w.r.t. these
models. Moreover BI logic is sound and complete w.r.t these models except for KR models, that is still
an open question [
11
].
From our notion of resource graph we also show that one can define a connection-based
characterization of BI’s validity with constraints without using prefixes like in other non-classical logics [
12
].
Moreover we study and define resource graphs for other logics and then provide a tableaux calculus
for BI’s Pointer logic (or SL) [
13, 14
], a new connection-based characterization of validity for Non
Commutative Logic [
15
] and also such a connection-based characterization for Bi-intuitionistic logic
(Bi-Int) with both implication and co-implication [
16
]. These works illustrate the interest to study
semantics and then to define and use constraints and resource graphs for designing calculi for different
resource logics.
We also mention works on semantics for Boolean BI (BBI) with the proposal of a Kripke relational
semantics for BBI (a non-deterministic monoidal semantics) with faithful embeddings of S4 and of
IL into BBI. It provides also a logical characterization of the observational power of BBI through an
adequate definition of bisimulation [
17
]. From this study of BBI semantics one can propose a labelled
tableau for BBI that is sound and also a sound and faithful embedding of BI into BBI [
18
]. In addition we
propose a complete phase semantics for BBI and an embedding between phase semantics for ILL and
Kripke semantics of BBI. By defining a fragment of ILL undecidable and complete for phase semantics
one can prove the undecidability of BBI [
19, 20
]. Concerning the labelled tableaux for partial monoidal
Boolean BI, it is important to note that the schema of its proof of strong completeness is original and it
has been completely formalized in Coq [
21
].
In the next part we present some modal extensions of (B)BI-based logics with different kinds of
modalities. A first one, called BI-Loc, considers a spatial modality for locations and resource trees and
proposes a new logic for resource distribution [
22
]. A second one, called DBI, extends BBI logic with
two modalities for expressing properties on states of process or on interacting systems. As the related
semantics introduces states in addition to resources, one also introduces state constraints in addition
to the resource constraints and then define a labelled tableaux calculus that is sound and complete
w.r.t. the semantics [
23
]. A third one, called DMBI (Dynamic Modal BI), is an extension of DBI for
introducing dynamics (resource transformations) with modalities à la Hennessy-Milner. Then new kinds
of constraints (resources, actions, states) are considered in the tableaux calculus that is proved sound
and complete w.r.t. the semantics [
24
]. A fourth one, called LSM, considers modalities, generalyzing S4
modalities. They are defined with two-dimensional worlds, one for S4 accessibility and one for resource
parametrization. and allow us to express properties of models of distributed computing. A sound and
complete labelled calculus is provided [
25
].
For these new modal separation logics we have mentioned modelling examples in order to illustrate their
expressivity and also the related labelled calculi with their properties of soundness and completeness.
We emphasize that the completeness proofs are based on the proof schema given in [
21
] for BBI logic,
that is extended and adapted, in a non-trivial way, for these logics.
In this context we also consider works on separation logics with knowledge and then propose some
epistemic extensions of BBI. One first, called ESL, considers epistemic modalities with a semantics
for which the possible (epistemic) worlds are resources that can be composed and decomposed. The
tableaux calculus for ESL is defined with resource constraints but also with agent constraints and it is
proved sound and complete w.r.t. the semantics [
26
]. The addition of public announcements modalities
to ESL has been also studied and results in a public announcement separation logic (PASL) [
27
].
Another epistemic extension of BBI, called ERL, deals with epistemic modalities that are parametrized
on agents’ local resources and allow us the modelling of some acces control problems. Let us note that
it is a conservative extension of BBI and Epistemic Logic. Again the study of the semantics and the
expressiveness has been completed by the design of a sound and complete labelled tableaux calculus [
28
].
We then continue this overview of BI and BBI modal and/or epistemic extensions, with a strong
focus on semantics and proof theory, by mentioning two works that benefit from some of the previous
results. A first work studies proof translations in BI logic between labelled and label-free calculi. The
results and their proofs emphasize the difficulty to design a translation from a proof in a labelled
calculus into a proof in a label-free calculus in BI logic, like in other logics. We expect that having a
general schema for such a translation would help us to prove a still open question for BI logic, that is
the completeness of the bunched calculus LBI w.r.t. KRM semantics [
29
].
A second work is about Separation Logic (SL) and inductive predicates. Proof systems for this logic are
often dedicated to some fragments of SL (symbolic heaps) that cannot express some properties about
pointers. They mainly allow either the full set of connectives, or the definition of arbitrary inductive
predicates, but not both. Then we comment a cyclic labelled system for SL that allows both [
30
]. This
work about cyclic proofs opens perspectives for some extensions of BI that will be developed in the
future. .
We conclude with a current work on a temporal extension of BI, called LTBI (Linear Time Bunched
Implication Logic) that is dedicated to resource evolution over time by combining BI separation
connectives and LTL temporal connectives [
31
]. A new semantics is given and a labelled calculus is defined
for LTBI and is proved sound but the completeness, proved for bounded timelines, is not trivial in
the general case of unbounded timelines. We expect that the definition of a cyclic proof system for
this logic would lead to the completeness result in this general setting. Finally we briefly present a
current study of new non-aggregative models of resource composition, namely compositions that do
not obey the principle that the whole is the sum of its parts. Our first objectives are to find algebraic
properties characterizing such compositions and then to design resource logics for such non-aggregative
compositions, if possible in the spirit of our previous works for BI, BBI and their extensions.