Search

Multi-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. We propose a simple inequational deduction system, based on term graphs, for inferring inclusions of derived relations in a multi-algebra, and we show that term graph rewriting provides a sound and complete implementation of it. © 2007 Elsevier B.V. All rights reserved.

We propose a framework for the verication of behavioural properties of systems modelled as graph transformation systems. The properties can be expressed in a temporal logic which is basically a -calculus where the state predicates are formulae of a monadic second order logic, describing graph properties. The verication technique relies on an algorithm for the construction of nite over-approximations of the unfolding of a graph transformation system.

We describe the design and the present state of the verification tool Augur 2 which is currently being developed. It is based on Augur 1, a tool which can analyze graph transformation systems by approximating them by Petri nets. The main reason for the new development was to create an open, flexible and extensible verification environment. Also, compared to the previous version, Augur 2 will include more functionality and new analysis techniques.

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.