A Model Checker for Bigraphs

We present a model checking tool for Bigraphical Reactive Systems that may be instantiated as a model checker for any formalism or domain-specific modelling language encoded as a Bigraphical Reactive System. We describe the implementation of the tool, and how it can be used to verify correctness properties of some infinite-state models by applying a static analysis to reaction rules that permits the exclusion of some infinite branches of execution shown to always be free of violations. We give a proof of correctness for this method, and illustrate the usage of the tool with two examples — a textbook implementation of the Dining Philosophers prob- lem, and an example motivated by a ubiquitous computing application.