European Association of Software Science and Technology

Log in
Workshop on Graph Transformation and Concurrency

Workshop on Graph Transformation and Concurrency

An informal workshop, to be held in Leicester on 24 - 26 January 2013, to discuss foundations and applications of concurrency in graph transformation.

Modelling and analysis of concurrent systems

  • Public

Modelling and analysis of concurrent systems

Started by Reiko Heckel 2015 days ago Replies (3)

Graphical rules can model distributed protocols in an intuitive and concise way, yet provide a formal specification amenable to verification.

  • Which problem domains are likely to benefit from such an approach to modelling? What properties do we want to verify there?
  • Are there case studies / benchmarks to validate such claims?
  • What are promising approaches to modelling and verification (language constructs used for modelling, methods and tools used for verification)?

Replies

  • Jan Stückrath 1988 days ago

    I am currently working on using the theory of well-structured transition systems for verification. Since our graph transformation systems have to be well-structured (with respect to some order), we are somewhat limited, but we hope to relax this restriction by introducing different orders more “compatible” with some classes of GTS. Approximation is also possible but currently not our focus.

    I could give a small introduction to our approach and explain what properties can be verified with it.

  • Jan Stückrath 1979 days ago

    I will give a brief introduction in: Verification of Well-Structured Graph Transformation Systems

    As already mentioned we use the theory of well-structured transition systems to solve the coverability problem for graph transformation systems. The idea is to have a property which is invariant with respect to the order and using the set of minimal graphs representing this property (which is finite). If one of the minimal graphs is coverable, a graph with the property can be reached from the initial graph. If we model errors in this way, we can verify for instance protols.

  • Dirk Janssens 1978 days ago

    Modeling concurrency by node replacement systems

     I would like to present a number of ideas for building a theory of true concurrency for graph rewriting systems based on node replacement, where the composition of processes replaces the traditional approach of building derivations as the basic way of describing system behavior. A first version of the framework is obtained by considering a very a basic kind of systems that uses pure node replacement, i.e. systems that deal with discrete, unlabeled graphs only. In spite of the fact that these are extremely simple they allow to introduce important notions such as processes, interaction, equivalence and composition (both on the level of individual  processes as on that of systems). Systems with a more reasonable expressivity can be obtained stepwise by introducing labels for nodes, edges and hyperedges, preserving the basic framework introduced for pure node replacement. Additional control, such as application conditions, can be added  as constraints on the set of valid processes. 

    The main advantage of the framework is, in my opinion,  that it is built on very simple mathematical tools, hopefully making it more accessible to potential users. It has been a problem for years that GT systems are seen as hard to understand; the phrase "iron harness" has been used in this respect. Some of the material has been published before, albeit in a quite different presentation.

    True Concurrency and Node Rewriting

Replies

In order to participate in this discussion, you must be a member of Workshop on Graph Transformation and Concurrency.