Abstract Interleaving Semantics for Reconfigurable Petri Nets

Abstract

Reconfigurable Petri nets are Petri nets together with rules for the dynamic change of the nets. We employ them for the formal modeling in the context of the Living Place Hamburg, a smart home that is an urban apartment serving as a laboratory for investigating different areas of ambient intelligence. The interaction of the resident and the smart home is modeled using informal descriptions of scenarios. These scenarios provide the resident's procedures together with the smart home's support. A case study using reconfigurable Petri nets for modeling these scenarios has required extensions of the theory and has clearly shown the need for an interleaving semantics for reconfigurable Petri nets. Scenarios are then given by nets, namely decorated place/transition nets that can be adapted to the evolving subgoals by applying rules that change the nets and hence the behavior of the smart home. Decorated place/transition nets are annotated place/transition nets with additional transition labels that may change when the transition is fired. To obtain such reconfigurable Petri nets we prove that decorated place/transition nets give rise to an M-adhesive HLR category. The abstract interleaving semantics we introduce is a graph with nodes that consist of an isomorphism class of the net structure and an isomorphism class of the current marking. Arcs between these nodes represent computation steps being either a transition firing or a direct transformation.