In: Farn Wang (Eds.): Lecture Notes in Computer Science, 3731: Formal Techniques for Networked and Distributed Systems - FORTE 2005: 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, pages 174-188. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1156243614,.
Abstract: Mobile systems explore the interplay between locality and connectivity. A subsystem may have a connection to a remote subsystem and use this for communication. Alternatively, it may be necessary or desirable to move the subsystem close to the other in order to communicate. This paper presents a Petri Net formalisation of mobile systems so as to harness the intuitive graphical representation of Petri Nets and the long history of associated analysis techniques. The proposed formalism starts with modular Petri Nets, where a net is divided into modules which can interact via place and transition fusion. The first change is that the flat module structure is replaced by fully nested modules, called locations. The nesting of locations provides a notion of locality while their fusion context determines their connectivity. The transitions constituting a location are constrained so that we can determine when a location is occupied by a subsystem, and when the subsystem shifts from one location to another. The colourless version of the formalism is conceptually simpler, while the coloured version caters for more dynamic configurations and helps identify isolated subsystems for which garbage collection may be appropriate.