On the Expressiveness of Mobile Synchronizing Petri Nets

In recent papers we have introduced Mobile Synchronizing Petri Nets, a new model for mobility based on coloured Petri Nets. It allows the description of systems composed of a collection of (possibly mobile) hardware devices and mobile agents, elled in a homogenous way and abstracting from middleware details. Our basic model introduced a colour to describe localities, but still lacked appropriate primitives to deal with security, and in fact it was equivalent to P/T nets. Then, we introduced the primitives to cope with security: a new colour for identifiers, basically corresponding to the natural numbers, that are created by means of a special transition. This mechanism allows us to deal with authentication issues. In this paper we discuss the expressiveness of the extended model with the authentication primitives. More specifically, we study several instances of the classical reachabilcoverability problems. Finally, we also study a more abstract version of the mechanism to create id...

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Fernando Rosa Velardo, David de Frutos-Escrig, Olga Marroquín Alonso
• Keywords: ENTCS 2007, Model, Petri Nets, Synchronizing Petri Nets