BI逻辑（Logic of Bunched Implications）是一种由Peter OHearn和DavidPym引入的子结构逻辑，它的主要用途是描述资源模型的性质并对其进行推理，尤其是包含指针等复杂数据类型的程序语言的性质。本文讨论了布尔BI逻辑的模型检查问题的可判定性与计算复杂性。证明了对递归定义的原子命题，模型检查问题即使对最简单的模型-有限生成自由幺半群一也是不可判定的。所使用的证明方法是将希尔伯特第十问题归约到本问题。本文进一步讨论了如下情况：所有出现的原子命题均为“生成元”命题。此时，有如下二分定理：如果布尔BI模型不是有限关系的，那么它的模型检查问题是不可判定的，这一部分结果通过将Minsky机的停机问题的归约到它来证明；否则它的模型检查问题是可判定的，并且是指数空间（EXPSPACE）完全的，其中，计算复杂性下界通过将幺半群中的字问题归约到这一问题得到，而上界由一个指数空间算法得到。　　 为了加强BI逻辑的表达能力，本文对BI逻辑进行了时态化扩展，称为时态BI逻辑。它可以良好地描述资源敏感的反应式系统所具有的性质。本文同时给出了它的模型检测问题的一些初步的结果。证明了对时态BI逻辑，它的模型检查问题也是不可判定的，即使限制到布尔情况，并且限制所有出现的原子命题均为“生成元”命题，以及状态-资源模型中的状态转移关系是资源无关的。这一不可判定结果同样通过将Minsky机的停机问题归约到本问题来证明。这也意味着时态BI逻辑的表达能力严格强于BI逻辑与时态逻辑CTL*。