On Model Checking Boolean BI

DOI10.1007/978-3-642-04027-6_23zbMath1257.03048OpenAlexW1580494308MaRDI QIDQ3644756

Yongzhi Cao, Zhongyuan Xu, Hanpin Wang, Heng Guo

Publication date: 12 November 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/47116998/mcBBI.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Undecidability of bisimilarity for Petri nets and some related problems
• Non-negative integer basis algorithms for linear equations with integer coefficients
• Adjunct elimination in context logic for trees
• On commutative Kleene monoids
• Decision problems for propositional linear logic
• Mobile ambients
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The complexity of the word problems for commutative semigroups and polynomial ideals
• Model checking mobile ambients
• Rational sets in commutative monoids
• Context logic as modal logic
• Quantitative Separation Logic and Programs with Lists
• The Logic of Bunched Implications
• Anytime, anywhere
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Classical BI
• Context logic and tree update
• Expressivity Properties of Boolean BI Through Relational Models
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Shorter Notes: Redei's Finiteness Theorem for Commutative Semigroups