Towards Model Checking Reconfigurable Petri Nets using Maude
Abstract
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.68.953
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.68.953.940
Hosted By Universitätsbibliothek TU Berlin.