On Model Checking Boolean BI

Heng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The logic of bunched implications (BI), introduced by O’Hearn and Pym, is a substructural logic which freely combines additive and multiplicative
implications. Boolean BI (BBI) denotes BI with classical interpretation of additives
and its model is the commutative monoid. We show that when the monoid
is finitely generated and propositions are recursively defined, or the monoid is
infinitely generated and propositions are restricted to generator propositions, the
model checking problem is undecidable. In the case of finitely related monoid and
generator propositions, the model checking problem is EXPSPACE-complete.
Original languageEnglish
Title of host publicationComputer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings
Number of pages15
Publication statusPublished - 28 Aug 2009
EventCSL 2009 - Coimbra, Portugal
Duration: 7 Sep 200911 Sep 2009


ConferenceCSL 2009
Internet address

Fingerprint Dive into the research topics of 'On Model Checking Boolean BI'. Together they form a unique fingerprint.

Cite this