1,721,119 research outputs found
High Level Replacement Systems applied to algebraic specifications and petri nets
No full textWorld Scientifi
Graph Abstraction for a Modal Logic
Full text linkWe are studying a particular graph abstraction, based on the concept of retaining neighbourhood information up to a certain radius for each node. In this contribution, we present a modal logic on graphs that is preserved and reflected by this abstraction. This is one of the main results from the EATCS Best Theoretical Paper at the International Conference on Graph Transformation 2008
Open Petri Nets: Non-deterministic Processes and Compositionality
No full textWe introduce ranked open nets, a reactive extension of Petri nets which generalises a basic open net model introduced in a previous work by allowing for a refined notion of interface. The interface towards the external environment of a ranked open net is given by a subset of places designated as open and used for composition. Additionally, a bound on the number of connections which are allowed on an open place can be specified. We show that the non-deterministic process semantics is compositional with respect to the composition operation over ranked open nets, a result which did not hold for basic open nets
Bisimilarity and and Behaviour-Preserving Reconfigurations of Open Petri Nets
No full textWe 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
Double-Pullback Transitions and Coalgebraic Loose Semantics for Graph Transformation Systems
No full textThe classical algebraic approach to graph transformation is a mathematical theory based on categorical techniques with several interesting applications in computer science. In this paper, a new semantics of graph transformation systems (in the algebraic, double-pushout (DPO) approach) is proposed in order to make them suitable for the specification of concurrent and reactive systems. Classically, a graph transformation system comes with a fixed behavioral interpretation. Firstly, all transformation steps are intended to be completely specified by the rules of the system, that is, there is an implicit frame condition: it is assumed that there is a complete control about the evolution of the system. Hence, the interaction between the system and its (possibly unknown) environment, which is essential in a reactive system, cannot be modeled explicitly. Secondly, each sequence of transformation steps represents a legal computation of the system, and this makes it difficult to model systems with control. The first issue is addressed by providing graph transformation rules with a loose semantics, allowing for unspecified effects which are interpreted as activities of the environment. This is formalized by the notion of double-pullback transitions, which replace (and generalize) the well-known double-pushout diagrams by allowing for spontaneous changes in the context of a rule application. Two characterizations of double-pullback transitions are provided: the first one describes them in terms of extended direct DPO derivations, and the second one as incomplete views of parallel or amalgamated derivations. The issue of constraining the behavior of a system to transformation sequences satisfying certain properties is addressed instead by introducing a general notion of logic of behavioral constraints, which includes instances like start graphs, application and consistency conditions, and temporal logic constraints. The loose semantics of a system with restricted behavior is defined as a category of coalgebras over a suitable functor. Such category has a final object which includes all finite and infinite transition sequences satisfying the constraints
Analysis of Permutation Equivalence in M-adhesive Transformation Systems with Negative Application Conditions
Full text linkpeer reviewedM-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and weak adhesive HLR categories and integrate high-level constructs such as attribution as in the case of typed attributed graphs.
In the current paper, we investigate -adhesive transformation systems including negative application conditions (NACs) for transformation rules, which are often used in applications. For such systems, we propose an original equivalence on transformation sequences, called permutation equivalence, that is coarser than the classical switch equivalence. We also present a general construction of deterministic processes for -adhesive transformation systems based on subobject transformation systems. As a main result, we show that the process obtained from a transformation sequence identifies its equivalence class of permutation-equivalent transformation sequences. Moreover, we show how the analysis of this process can be reduced to the analysis of the reachability graph of a generated Place/Transition Petri net. This net encodes the dependencies between rule applications of the transformation sequence, including the inhibiting effects of the NACs
Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets
No full textIn the framework of graph transformation systems with Negative Application
Conditions (NACs) the classical notion of switch equivalence of derivations
is extended to permutation equivalence, because there are intuitively equivalent
derivations which are not switch-equivalent if NACs are considered. By definition,
two derivations are permutation-equivalent, if they respect the NACs and
disregarding the NACs they are switch equivalent. A direct analysis of permutation
equivalence is very complex in general, thus we propose a much more efficient analysis
technique. For this purpose, we construct a Place/Transition Petri net, called
dependency net, which encodes the dependencies among rule applications of the
derivation, including the inhibiting effects of the NACs.
The analysis of permutation equivalence is important for analysing simulation runs
within development environments for systems modelled by graph transformation.
The application of the technique is demonstrated by a graph transformation system
within the context of workflow modelling. We show the effectiveness of the approach
by comparing the minimal costs of a direct analysis with the costs of the
efficient analysis applied to a derivation of our example system
- …
