| Authors: Harmen Kastenberg Affiliation: University of Twente (Netherlands) Title: Toward Attributed Graphs in Groove (work-in-progress) Abstract: Graphs are a very expressive formalism for system odeling, especially when attributes are allowed. Our research is mainly focussed on the use of graphs for system verification. Up to now, there are two main different approaches of modeling (typed) attributed graphs and specifying their transformation. Here we report preliminary results of our investigation on a third approach of modeling attributed graphs. In our approach we couple a graph to a data signature that consists only of unary operations. Therefore, we transform arbitrary signatures into a structure comparable to what is called a graph structure signature in the literature, and arbitrary algebras into the corresponding algebra graph. Some advantages of our approach are, firstly, that the graphical representation we introduce for transforming the data part part of attributed graphs has a close relation with the signature structure we use. Secondly, in our approach we do not need to introduce an additional set of variables to reason about data since we can re-use ordinary rule nodes to stand for data values. Furthermore, we do not put any restrictions on the algebraic semantics of the specified operations. We assume that this information is provided by the algebra graph. In this report we use a simple example to explain how we model attributed graphs and their transformation and to describe the advantages listed before. |
| Authors: Bilel Derbel, Mohamed
Mosbah Affiliation: LaBRI - University of Bordeaux 1 (FRANCE) Title: Distributed Graph Traversals by Relabeling Systems with Applications Abstract: Graph traversals are in the basis of many distributed algorithms. In this paper, we use graph relabelling systems to encode two basic graph traversals which are the broadcast and the convergecast. This encoding allows us to derive formal, modular and simple encoding for many distributed graph algorithms. We illustrate this method by investigating the distributed computation of a BFS tree and the distributed computation of a minimum spanning tree. Our formalism allows to focus on the correctness of a distributed algorithm rather than on the implementation and the communication details. |
| Authors: Fabio Gadducci,
Alberto Lluch-Lafuente Affiliation: University of Pisa (Italy) Title: Graphical Verification of a Spatial Logic for the pi-calculus Abstract: The paper introduces a novel approach to the verification of spatial properties for finite pi-calculus specifications. The mechanism is based on a recently proposed graphical encoding for mobile calculi: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Spatial properties for reasoning about the behavior and the structure of pi-calculus processes are then expressed in a logic introduced by Caires, and they are verified on the graphical encoding of a process, rather than on its textual representation. More precisely, the graphical presentation allows for (i) obtaining a faithful translation of spatial formulae into (a modal extension of a fragment of) Courcelle`s monadic second order logics (so that a process verifies a spatial formula exactly when its graphical representation verifies the translated formula); and (ii) providing a simple and easy to implement verification algorithm based on the graphical encoding (returning true if and only if a given process verifies a given spatial formula). |
| Authors: Dobieslaw Wroblewski Affiliation: ICS PAS (Poland) Title: Semi-local model of computations on graphs to break the local symmetry (work-in-progress) Abstract: We consider connected undirected graphs without self-loops as a model of computer networks. The nodes of the graph represent computers or processors, while the edges of the graph correspond to the links between them. We present a new model of distributed computations, called semi-local. This extension of the classical local model breaks the local symmetry. As a result, many useful tasks become deterministically solvable in every network assuming a very small initial knowledge about its graph representation. One of these tasks is a creation of a token in an arbitrary anonymous ring - an example of election of a leader. A semi-local solution to this problem is presented. |
| Authors: Mikkel Bundgaard,
Thomas Hildebrandt Affiliation: IT University of Copenhagen (Denmark) Title: Bigraphical Semantics of Higher-order Mobile Embedded Resources with Local Names Abstract: Bigraphs have been introduced with the aim to provide a topographical meta-model for mobile, distributed agents that can manipulate their own linkages and nested locations, generalising both the dynamic linking characteristic to the pi-calculus and the dynamic nested locations characteristic to the Mobile Ambients calculus. We give the first bigraphical presentation of a non-linear, higher-order process calculus with nested locations, active process mobility and local names, the calculus of Higher-Order Mobile Embedded Resources (Homer). The presentation generalises Milner`s recent presentation of the lambda-calculus in local bigraphs. The presentation shows that the combination of non-linear, active process mobility and local names needs special care. In particular, we need to introduce a new definition of parametric reaction rules. We conclude by suggesting a generalisation of local bigraphs in which links can be further localised, which allows a more direct representation of non-linear, active process mobility with local names. |
| Authors: Ivan Lanese, Ugo
Montanari Affiliation: Computer Science Department-University of Pisa (Italy) Title: Hoare vs Milner: comparing synchronizations in a graphical framework with mobility Abstract: We compare the expressive power of Hoare (i.e., CSP style) and Milner (i.e., CCS style) synchronizations for defining graph transformations in a framework where edges can perform actions on adjacent nodes to synchronize their evolutions. Furthermore, nodes can be communicated and merged. We show that the expressive powers of the two synchronization models are different, but no one is greater than the other. Finally, we show that in many interesting cases the behaviour of a synchronization model can be mimicked by the other one using suitable translations for the rewritten graphs. |
| Authors: Mike Dodds, Detlef Plump Affiliation: Department of Computer Science (United Kingdom) Title: Extending C for Checking Shape Safety (work-in-progress) Abstract: The project Safe Pointers by Graph Transformation at the University of York has developed a method for specifying the shape of pointer-data structures by graph reduction, and a static checking algorithm for proving the shape safety of graph transformation rules modelling operations on pointer structures. In this paper, we outline how to apply this approach to the C programming language. We extend ANSI C with so-called transformers which model graph transformation rules, and with shape specifications for pointer structures. For the resulting language C-GRS, we present both a translation to C and and an abstraction to graph transformation. Our main result is that the abstraction of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation. |
| Authors: Sebastian Menge,
Georgios Lajios Affiliation: University of Dortmund, Software-Technology (Germany) Title: An integration tool for Stochastic Graph Transformation (work-in-progress) Abstract: Stochastic Graph Transformation combines the benefits of graphical modelling with stochastic analysis techniques. In this paper we report on SGT*, an integration tool that separates the modelling of stochastic systems from their analysis. We present the tool`s architecture together with experiences and perspectives. |