(PAPER WITHDRAWN) An Improvement for BigMC
- 10.2991/icmmita-16.2016.187How to use a DOI?
- bigraph; bigraphical reactive system; Model checking; Matching of bigraph; Bigraph model checking;
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.
- © 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/).
Cite this article
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 -