(PAPER WITHDRAWN) An Improvement for BigMC

DOI

10.2991/icmmita-16.2016.187How to use a DOI?

Keywords

bigraph; bigraphical reactive system; Model checking; Matching of bigraph; Bigraph model checking;

Abstract

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.

Copyright

© 2017, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Qing-Quan Shi
PY  - 2017/01
DA  - 2017/01
TI  - (PAPER WITHDRAWN) An Improvement for BigMC
BT  - Proceedings of the 2016 4th International Conference on Machinery, Materials and Information Technology Applications
PB  - Atlantis Press
SN  - 2352-538X
UR  - https://doi.org/10.2991/icmmita-16.2016.187
DO  - 10.2991/icmmita-16.2016.187
ID  - Shi2017/01
ER  -