Dagstuhl Seminar Proceedings, Volume 4241
Dagstuhl Seminar Proceedings
DagSemProc
https://www.dagstuhl.de/dagpub/1862-4405
https://dblp.org/db/series/dagstuhl
1862-4405
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
4241
2005
https://drops.dagstuhl.de/entities/volume/DagSemProc-volume-4241
04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
Recently there has been a lot of research, combining concepts of process algebra with those of the theory of graph grammars and graph transformation systems. Both can be viewed as general frameworks in which one can specify and reason about concurrent and distributed systems. There are many areas where both theories overlap and this reaches much further than just using graphs to give a graphic representation to processes.
Processes in a communication network can be seen in two different ways: as terms in an algebraic theory, emphasizing their behaviour and their interaction with the environment, and as nodes (or edges) in a graph, emphasizing their topology and their connectedness. Especially topology, mobility and dynamic reconfigurations at
runtime can be modelled in a very intuitive way using graph transformation. On the other hand the definition and proof of behavioural equivalences is often easier in the process algebra setting.
Also standard techniques of algebraic semantics for universal constructions, refinement and compositionality can take better advantage of the process algebra representation. An important example where the combined theory is more convenient than both alternatives is for defining the concurrent (noninterleaving), abstract semantics of distributed systems. Here graph transformations lack abstraction and process algebras lack expressiveness.
Another important example is the work on bigraphical reactive systems with the aim of deriving a labelled transitions system from an unlabelled reactive system such that the resulting bisimilarity is a congruence. Here, graphs seem to be a convenient framework, in which this theory can be stated and developed.
So, although it is the central aim of both frameworks to model and reason about concurrent systems, the semantics of processes can have a very different flavour in these theories. Research in this area aims at combining the advantages of both frameworks and translating concepts of one theory into the other. The Dagsuthl Seminar, which took place from 06.06. to 11.06.2004, was aimed at bringing together researchers of the two communities in order to share their ideas and develop new concepts. These proceedings4 of the do not only contain abstracts of the talks given at the seminar, but also summaries of topics of central interest. We would like to thank all participants of the seminar for coming and sharing their ideas and everybody who has contributed to the proceedings.
graph transformation
process calculi
0-0
Regular Paper
Barbara
König
Barbara König
Ugo
Montanari
Ugo Montanari
Philippa
Gardner
Philippa Gardner
10.4230/DagSemProc.04241.1
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences
This paper is intended as a short informal summary of some
of the topics which arose at the Dagstuhl meeting held 6/06/04-11/06/04.
In particular, we shall summarise some of the content of talks by H. Ehrig, F. Gadducci, O. H. Jensen, R. Milner, B. KÃ?Â¶nig,
V. Sassone and the author. The general areas include adhesive
categories and generalisations, contextual labelled transition semantics
for graph transformation systems via borrowed-contexts and GIPOs, and
bigraphs. We shall conclude with a summary of some of the discussions
which followed the aforementioned presentations.
graph transformation
category theory
bisimulation
1-12
Regular Paper
Pawel
Sobocinski
Pawel Sobocinski
10.4230/DagSemProc.04241.2
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Summary 2: Graph Grammar Verification through Abstraction
Until now there have been few contributions concerning the
verification of graph grammars, specifically of infinite-state graph
grammars. This paper compares two existing approaches, based on
abstractions of graph transformation systems. While in the unfolding
approach graph grammars are approximated by Petri nets, in the
partitioning approach graphs are abstracted according to their local
structure. We describe differences and similarities of the two
approaches and explain the underlying ideas.
graph transformation
verification
1-9
Regular Paper
Paolo
Baldan
Paolo Baldan
Barbara
König
Barbara König
Arend
Rensink
Arend Rensink
10.4230/DagSemProc.04241.3
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Summary 3: On Graph(ic) Encodings
This paper is an informal summary of different encoding techniques
from process calculi and distributed formalisms to graphic frameworks. The survey
includes the use of solo diagrams, term graphs, synchronized hyperedge replacement
systems, bigraphs, tile models and interactive systems, all presented at
the Dagstuhl Seminar 04241. The common theme of all techniques recalled here
is having a graphic presentation that, at the same time, gives both an intuitive visual
rendering (of processes, states, etc.) and a rigorous mathematical framework.
graph transformation
process calculi
encodings
1-15
Regular Paper
Roberto
Bruni
Roberto Bruni
Ivan
Lanese
Ivan Lanese
10.4230/DagSemProc.04241.4
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode