Satisfaction, Restriction and Amalgamation of Constraints in the Framework of M-Adhesive Categories
Authors:
Hanna Schölzel,
Hartmut Ehrig,
Maria Maximova,
Karsten Garbriel,
Frank Hermann
Abstract:
Application conditions for rules and constraints for graphs are well-known in the theory of graph transformation and have been extended already to M-adhesive transformation systems. According to the literature we distinguish between two kinds of satisfaction for constraints, called general and initial satisfaction of constraints, where initial satisfaction is defined for constraints over an initia…
▽ More
Application conditions for rules and constraints for graphs are well-known in the theory of graph transformation and have been extended already to M-adhesive transformation systems. According to the literature we distinguish between two kinds of satisfaction for constraints, called general and initial satisfaction of constraints, where initial satisfaction is defined for constraints over an initial object of the base category. Unfortunately, the standard definition of general satisfaction is not compatible with negation in contrast to initial satisfaction.
Based on the well-known restriction of objects along type morphisms, we study in this paper restriction and amalgamation of application conditions and constraints together with their solutions. In our main result, we show compatibility of initial satisfaction for positive constraints with restriction and amalgamation, while general satisfaction fails in general.
Our main result is based on the compatibility of composition via pushouts with restriction, which is ensured by the horizontal van Kampen property in addition to the vertical one that is generally satisfied in M-adhesive categories.
△ Less
Submitted 6 September, 2012;
originally announced September 2012.
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
Authors:
Paolo Baldan,
Andrea Corradini,
Hartmut Ehrig,
Reiko Heckel,
Barbara König
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 bisimilarity…
▽ More
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 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.
△ Less
Submitted 21 October, 2008; v1 submitted 24 September, 2008;
originally announced September 2008.
