0809.4115.pdf (881.83 kB)
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
journal contribution
posted on 2012-10-24, 09:06 authored by P. Baldan, A. Corradini, H. Ehrig, Reiko Heckel, B. KoenigWe 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 bisimilarity over open nets are congruences with respect to the composition operation. The considered behavioural equivalences differ for the choice of the observations, which can be single firings or parallel steps. Additionally, we consider weak forms of such equivalences, arising in the presence of unobservable
actions. 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.
Funding
Research partially supported by the EU IST-2004-16004 SEnSOria, the MIUR Project ART, the DFG project SANDS, the DFG project Behaviour-GT and CRUI/DAAD Vigoni “Models based on Graph Transformation Systems: Analysis and Verification”.
History
Citation
Logical Methods in Computer Science, 2008, 4 (4)Published in
Logical Methods in Computer SciencePublisher
IfCoLog (International Federation of Computational Logic)issn
1860-5974Available date
2012-10-24Publisher DOI
Publisher version
http://www.lmcs-online.org/ojs/viewarticle.php?id=384Notes
1998 ACM Subject Classification: F.3.1, F.4.2.Language
EnglishAdministrator link
Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC