Coding Mobile Synchronizing Petri Nets into Rewriting Logic

Mobile Synchronizing Petri Nets (MSPN's) are a model for mobility and coordination based on coloured Petri Nets, in which systems are composed of a collection of (possibly mobile) hardware devices and mobile agents, both modelled homogenously. In this paper we approach their verification, for which we have chosen to code MSPN's into rewriting logic. In order to obtain a representation of MSPN systems by means of a rewrite theory, we develop a class of them, that we call ν-Abstract Petri nets (ν-APN's), which are easily representable in that framework. Moreover, the obtained representation provides a local mechanism for fresh name generation. Then we prove that, even if ν-APN's are a particular class of MSPN systems, they are strong enough to capture the behaviour of any MSPN system. We have chosen Maude to implement ν-APN's, as well as the translation from MSPN's to ν-APN's, for which we make intensive use of its reflective features