5th International Workshop on Petri Nets,  Graph Transformation and other 

Concurrency Formalisms

PNGT 2012

September 29, 2012
Bremen, Germany

http://www.informatik.haw-hamburg.de/PNGT2012.html
raven

A Satellite Event of ICGT 2012


SCHEDULE
9:00-10:00
Invited Talk:  Conditional Reactive Systems Barbara König
10:15 - 10:45
10:45 - 11:15
11:15 - 11:45 
Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M-Functors  Maria Maximova, Hartmut Ehrig, Claudia Ermel
Process Evolution based on Transformation of Algebraic High-Level Nets with Applications to Communication Platforms Karsten Gabriel
On Modelling Communication in Ubiquitous Computing Systems using Algebraic Higher Order Nets Susann Gottmann, Nico Nachtigall, Kathrin Hoffmann
12:15 - 12:45 
12:45 - 13:15 
Optimization in Graph Transformation Systems with Time Using Petri Net Based Techniques Szilvia Varró-Gyapay
Abstract Interleaving Semantics for Reconfigurable Petri Nets Julia Padberg
Abstracts: Conditional Reactive Systems
Barbara König

Reactive Systems were introduced by Leifer and Milner. They provide a general categorical setting for modelling abstract rewriting:  graph transformation systems, process calculi and also Petri nets can be seen as special cases of reactive systems.
In this talk the notion of nested application conditions will be lifted from graph transformation systems to the setting of reactive systems.  This serves two purposes: first, we enrich the formalism of reactive systems by adding application conditions for rules; second, it turns out that some constructions for graph transformation systems (such as computing weakest preconditions and strongest postconditions and showing local confluence by means of critical pair analysis) can be done elegantly in the more general setting.

Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M-Functors

Maria Maximova, Hartmut Ehrig, Claudia Ermel
Recently, a formal relationship between Petri net and graph transformation systems has been established using the new framework of M-functors F: (C1,M1) -> (C2,M2) between M-adhesive categories. This new approach allows us to translate transformations in (C1,M1) into corresponding transformations in (C2,M2) and, vice versa, to create transformations in (C1,M1) from those in (C2,M2). In this paper, we extend this framework to the transfer of local confluence, termination and functional behavior. In particular, we are able to create these properties for transformations in (C1,M1) from corresponding properties of transformations in (C2,M2), where (C1,M1) are Petri nets with individual tokens and (C2,M2) typed attributed graphs. This allows us to apply the well-known critical pair analysis for typed attributed graph transformations supported by the AGG-tool
in order to analyze these properties for Petri net transformations.

Process Evolution based on Transformation of Algebraic High-Level Nets with Applications to Communication Platforms
Karsten Gabriel
Algebraic High-Level (AHL) nets are a well-known modelling technique based on Petri nets with algebraic data types, which allows to model the communication structure and the data flow within one modelling framework. Transformations of AHL-nets -- inspired by the theory of graph transformations -- allow in addition to modify the communication structure. Moreover, high-level processes of AHL-nets capture the concurrent semantics of AHL-nets in an adequate way. Altogether we obtain a powerful integrated formal specification technique to model and analyse all kinds of communication based systems, especially different kinds of communication platforms.  In this paper we show how to model the evolution of communication platforms and scenarios based on transformations of Algebraic High-Level Nets and Processes. All constructions and results are illustrated by a running example showing the evolution of Apache Wave platforms and scenarios. The evolution of platforms is modelled by the transformation of AHL-nets and that of scenarios by the transformation of AHL-net processes.  Our main result is a construction for the evolution of AHL-processes based on the evolution of the corresponding AHL-net. This result can be used to transform scenarios in a communication platform according to the evolution of possibly multiple actions of the platform.

On Modelling Communication in Ubiquitous Computing Systems using Algebraic Higher Order Nets

Susann Gottmann, Nico Nachtigall and Kathrin Hoffmann
Ubiquitous computing systems (UCSs) are designed to participate almost imperceptibly in everyday life. To ensure a solid operation, a UCS heavily relies on a reliable and efficient communication between its distributed computing components where components can join and leave the system at any time. In order to guarantee high quality systems, the use of models is inevitable especially at an early stage of the development process where models are the only possibility to address a system which does not yet exist in reality. Petri nets and graph transformation systems are established, theoretically well-founded concepts for modelling and analysing complex systems.This paper presents a formal approach for modelling core aspects of the communication in UCSs by using algebraic higher-order nets with individual tokens and graph transformation. In contrast to a wide range of other modelling techniques, this approach is suitable to cover the different aspects of communication in an integrative form and enables the analysis of specific properties. The approach and its suitability are illustrated based on a running example. The feasibility of embedding the approach in a broader context of modelling is demonstrated in applying it to a real world system: the Living Place Project.

Optimization in Graph Transformation Systems with Time Using Petri Net Based Techniques

Szilvia Varró-Gyapay
Extra-functional properties of IT systems have to be analyzed and subsequently optimized carefully during the design phase in order to assure a proper quality of service and decrease operational costs. Several verification and validation methods are known to check the correctness of the system services, while optimization may serve to reach boundaries thus minimizing costs or duration of operating the system. However, the combination of the best practices of the two fields according to
the purpose of the analysis is a challenging question. In a previous paper, we showed how such a problem can be formalized and solved when the evolution of the system is captured by graph transformation systems (GTS) with cost parameters attached to each graph transformation rule denoting the cost of firing the rule. This technique is adapted in the current paper to deliver a time-optimal trajectory in a GTS with time. While the cost of a GT rule sequence always equals to the sum of the cost of the involved GT rules, the concurrent application of GT rules may reduce the minimal duration of a GT rule sequence, which is a major conceptual difference concerning optimization.

Abstract Interleaving Semantics for Reconfigurable Petri Nets

Julia Padberg
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.
The case study using reconfigurable Petri nets for modeling these scenarios has led to necessary extensions of the theory and has clearly shown the need for an interleaving semantics of the reconfigurable Petri nets. Scenarios are then given by nets, namely decorated 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 P/T nets with additional transition labels that may change when the transition is fired. To obtain reconfigurable Petri nets based on these decorated P/T nets we prove that they give rise to a M-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 actual marking. Arcs between these node represent computation steps being either a transition firing or a direct transformation.