On Model Checking Boolean BI
From MaRDI portal
Decidability of theories and sets of sentences (03B25) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- Nondeterministic phase semantics and the undecidability of Boolean BI
- Expressivity Properties of Boolean BI Through Relational Models
- The semantics and proof theory of the logic of bunched implications
- scientific article; zbMATH DE number 2242591
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
Cites work
- Adjunct elimination in context logic for trees
- Anytime, anywhere: modal logics for mobile ambients
- Classical BI
- Context logic and tree update
- Context logic as modal logic, completeness and parametric inexpressivity
- Decision problems for propositional linear logic
- Expressivity Properties of Boolean BI Through Relational Models
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- scientific article; zbMATH DE number 1701350 (Why is no real title available?)
- scientific article; zbMATH DE number 176134 (Why is no real title available?)
- scientific article; zbMATH DE number 1948162 (Why is no real title available?)
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 1841829 (Why is no real title available?)
- scientific article; zbMATH DE number 3216273 (Why is no real title available?)
- scientific article; zbMATH DE number 3284302 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- Mobile ambients
- Model checking mobile ambients
- Non-negative integer basis algorithms for linear equations with integer coefficients
- On commutative Kleene monoids
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Quantitative Separation Logic and Programs with Lists
- Rational sets in commutative monoids
- Shorter Notes: Redei's Finiteness Theorem for Commutative Semigroups
- The complexity of the word problems for commutative semigroups and polynomial ideals
- The Logic of Bunched Implications
- Undecidability of bisimilarity for Petri nets and some related problems
Cited in
(6)- A theorem prover for Boolean BI
- Nondeterministic phase semantics and the undecidability of Boolean BI
- Looking at separation algebras with Boolean BI-eyes
- scientific article; zbMATH DE number 4178463 (Why is no real title available?)
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- Expressivity Properties of Boolean BI Through Relational Models
This page was built for publication: On Model Checking Boolean BI
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3644756)
