An Improvement for BigMC

摘要

Bigraph which proposed by Robin Milner is a powerful formalized modeling language. We can get the bigraphical reactive systems (BRS) by using bigraph to represent each state in a system. Model checking is the technology which can verify whether a given model stratifies the specified requirement and it's helpful to promote the application of bigraph in reality if we apply the ideas of model checking to BRS. At present, there almost has no bigraph model checking tool except the BigMC that developed by Gian Perron. However, the term language of bigraph that proposed by Gian Perron is not complete (it lacks inner names and edges) and the model checking algorithm is not efficient as well as there are some incorrectness in his handle of state explosion. In this paper, we make some improvements on the term language of bigraph and point out the incorrectness. What's more, new definitions and optimizations are proposed. At last, some specific instances are presented to illustrate the bigraph model checking in this paper.