On Model Checking Boolean BI

Heng Guo; Hanpin Wang; Zhongyuan Xu; Yongzhi Cao

doi:10.1007/978-3-642-04027-6_23

On Model Checking Boolean BI

Heng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings
Pages	302-316
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-04027-6_23
Publication status	Published - 28 Aug 2009
Event	CSL 2009 - Coimbra, Portugal Duration: 7 Sep 2009 → 11 Sep 2009 http://www.mat.uc.pt/~csl/

Conference

Conference	CSL 2009
Country	Portugal
City	Coimbra
Period	7/09/09 → 11/09/09
Internet address	http://www.mat.uc.pt/~csl/

Access to Document

10.1007/978-3-642-04027-6_23

mcBBIAccepted author manuscript, 113 KB

https://link.springer.com/chapter/10.1007%2F978-3-642-04027-6_23

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

Cite this

@inproceedings{fab032a569e347c9bf6b3d1aadeef79f,

title = "On Model Checking Boolean BI",

abstract = "The logic of bunched implications (BI), introduced by O{\textquoteright}Hearn and Pym, is a substructural logic which freely combines additive and multiplicativeimplications. Boolean BI (BBI) denotes BI with classical interpretation of additivesand its model is the commutative monoid. We show that when the monoidis finitely generated and propositions are recursively defined, or the monoid isinfinitely generated and propositions are restricted to generator propositions, themodel checking problem is undecidable. In the case of finitely related monoid andgenerator propositions, the model checking problem is EXPSPACE-complete.",

author = "Heng Guo and Hanpin Wang and Zhongyuan Xu and Yongzhi Cao",

year = "2009",

month = aug,

day = "28",

doi = "10.1007/978-3-642-04027-6_23",

language = "English",

pages = "302--316",

booktitle = "Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings",

note = "CSL 2009 ; Conference date: 07-09-2009 Through 11-09-2009",

url = "http://www.mat.uc.pt/~csl/",

}

TY - GEN

T1 - On Model Checking Boolean BI

AU - Guo, Heng

AU - Wang, Hanpin

AU - Xu, Zhongyuan

AU - Cao, Yongzhi

PY - 2009/8/28

Y1 - 2009/8/28

N2 - The logic of bunched implications (BI), introduced by O’Hearn and Pym, is a substructural logic which freely combines additive and multiplicativeimplications. Boolean BI (BBI) denotes BI with classical interpretation of additivesand its model is the commutative monoid. We show that when the monoidis finitely generated and propositions are recursively defined, or the monoid isinfinitely generated and propositions are restricted to generator propositions, themodel checking problem is undecidable. In the case of finitely related monoid andgenerator propositions, the model checking problem is EXPSPACE-complete.

AB - The logic of bunched implications (BI), introduced by O’Hearn and Pym, is a substructural logic which freely combines additive and multiplicativeimplications. Boolean BI (BBI) denotes BI with classical interpretation of additivesand its model is the commutative monoid. We show that when the monoidis finitely generated and propositions are recursively defined, or the monoid isinfinitely generated and propositions are restricted to generator propositions, themodel checking problem is undecidable. In the case of finitely related monoid andgenerator propositions, the model checking problem is EXPSPACE-complete.

U2 - 10.1007/978-3-642-04027-6_23

DO - 10.1007/978-3-642-04027-6_23

M3 - Conference contribution

SP - 302

EP - 316

BT - Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings

T2 - CSL 2009

Y2 - 7 September 2009 through 11 September 2009

ER -