On Model Checking Boolean BI

Heng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao

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

Abstract

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
Pages302-316
Number of pages15
DOIs
Publication statusPublished - 28 Aug 2009
EventCSL 2009 - Coimbra, Portugal
Duration: 7 Sep 200911 Sep 2009
http://www.mat.uc.pt/~csl/

Conference

ConferenceCSL 2009
CountryPortugal
CityCoimbra
Period7/09/0911/09/09
Internet address

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

Cite this