A Model Checker for Bigraphs

Gian David Perrone, Søren Debois, Thomas Hildebrandt

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationSAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication dateMar 2012
ISBN (Print)978-1-4503-0857-1
Publication statusPublished - Mar 2012
EventACM Symposium on Applied Computing 2012 - Riva del Garda, Italy
Duration: 26 Mar 201230 Mar 2012
Conference number: 27th


ConferenceACM Symposium on Applied Computing 2012
CityRiva del Garda
Internet address


  • Model Checking
  • Bigraphical Reactive Systems
  • Formal Verification
  • Infinite-State Models
  • Static Analysis


Dive into the research topics of 'A Model Checker for Bigraphs'. Together they form a unique fingerprint.

Cite this