Skip to content
master
Go to file
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
bin
 
 
 
 
doc
 
 
 
 
m4
 
 
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

README

BigMC (Bigraphical Model Checker) is a model-checker designed to operate on Bigraphical Reactive Systems (BRS). BRS is a formalism developed by Robin Milner and colleagues that emphasises the orthogonal notions of locality and connectivity. Bigraphs have found applications in ubiquitous computing, computational biology, business workflow modelling, and context-aware systems.

By model checking, we mean precisely the act of checking whether some specification is true of a particular bigraphical model. This is achieved through a kind of exhaustive search of all the possible states of the system. For arbitrary models, this kind of checking is computationally intractable, as the state space is simply too huge (and indeed infinite in many cases). The challenge of this kind of task is to limit the kinds of models we check to some tractable subset, and to reduce the number of actual states that we need to check directly in order to provide concrete correctness guarantees.

You can’t perform that action at this time.