On Model Checking Boolean BI

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

Heng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao

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

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

03B25: Decidability of theories and sets of sentences

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

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