ECEASST Abstract Interleaving Semantics for Reconfigurable Petri Nets

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 re-quired extensions of the theory and has clearly shown the need for an interleaving se-mantics for reconfigurable Petri nets. Scenarios are then given by nets, namely dec-orated 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 la-bels that may change when the transition is fired. To obtain such reconfigurable Petri nets we prove that decorated place/transition nets give rise to anM-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 cur-rent marking. Arcs between these nodes represent computation steps being either a transition firing or a direct transformation