Local State Refinement and Composition of Elementary Net Systems: An Approach Based on Morphisms

In the design of concurrent and distributed systems, modularity and refinement are basic conceptual tools. We propose a notion of refinement/abstraction of local states for a basic class of Petri Nets, associated with a class of morphisms. The morphisms, from a refined system to an abstract one, associate suitable subnets to abstract local states. We define an operation of composition ruled by morphisms of that class. The main results concern behavioural properties preserved and reflected by the morphisms. In particular, we focus on the conditions under which reachable markings are preserved or reflected, and the conditions under which a morphism induces a weak bisimulation between net systems.