Expressivity properties of Boolean BI through relational models

The work

AuthorsDidier Galmiche; Dominique Larchey-Wendling
Editors
Typeinproceedings
Year2006
Citekeygalmiche2006expressivity

Where it appeared

Published in26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
PublisherSpringer
Volume4337
Pages357--368

Identifiers

DOI10.1007/11944836_33

Abstract

In this paper, we study Boolean BI Logic (BBI) from a semantic per- spective. 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 re- sults 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 intuition- istic 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.

A copy is held

pdf, 164.1 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-12 13:50 UTC

Filed under

separation-logic the-copy-is-not-the-work

Cite it as

@inproceedings{galmiche2006expressivity,
  title        = {Expressivity properties of Boolean BI through relational models},
  author       = {Didier Galmiche and Dominique Larchey-Wendling},
  year         = {2006},
  booktitle    = {26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)},
  publisher    = {Springer},
  volume       = {4337},
  pages        = {357--368},
  doi          = {10.1007/11944836_33},
}

This record lives at https://refs.drheap.org/galmiche2006expressivity/ and will keep doing so.