出版社:European Association of Software Science and Technology (EASST)
摘要:This paper introduces an approach to model checking of reconfigurable Petri nets. The main task is to flatten the two levels of dynamic behavior that reconfigurable nets provide, the firing of transitions on the one hand and the transformation of the nets on the other hand. We show how to translate a reconfigurable net into Maude modules. Maude's LTL model-checker is then used to verify properties of these modules.