Bisimilarity and Behaviour Preserving Reconfigurations
of Open petri Nets
P. Baldan(1), A. Corradini(2), H. Ehrig(3), R. Heckel(4), B. Koenig(5)
(1)Dipartimento di Informatica, Università di Pisa, Italy
(2)Computer Science Department, University Ca' Foscari of Venice (Italy)
(3)Computer Science Department, Technical University of Berlin (Germany)
(4)Department of Computer Science, University of Leicester (UK)
(5)Institut fuer Informatik und interaktive Systeme,
Universitaet
Duisburg-Essen (UK)
Abstract:
We propose a framework for the specification of behaviour-preserving
reconfigurations of systems modelled as Petri nets. The framework is
based on open nets, a mild generalisation of ordinary
Place/Transition nets suited to model open systems which might
interact with the surrounding environment and endowed with a
colimit-based composition operation. We show that natural notions of
(strong and weak) bisimilarity over open nets are congruences with
respect to the composition operation. We also provide an up-to
technique for facilitating bisimilarity proofs. The theory is used
to identify suitable classes of reconfiguration rules (in the
double-pushout approach to rewriting) whose application preserves
the observational semantics of the net.