Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Expressivity Properties of Boolean BI Through Relational Models
verfasst von : Didier Galmiche, Dominique Larchey-Wendling
Erschienen in: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we study Boolean
BI
Logic (
BBI
) from a semantic perspective. This logic arises as a logical basis of some recent separation logics used for reasoning about mutable data structures and we aim at proposing new results from alternative semantic foundations for
BBI
that seem to be necessary in the context of modeling and proving program properties. Starting from a Kripke relational semantics for
BBI
which can also be viewed as a non-deterministic monoidal semantics, we first show that
BBI
includes some S4-like modalities and deduce new results: faithful embeddings of
S4
modal logic, and then of intuitionistic logic (
IL
) into
BBI
, despite of the classical nature of its additive connectives. Moreover, we provide a logical characterization of the observational power of
BBI
through an adequate definition of bisimulation.