Graph grammars or graph transformation systems (GTS), originally
introduced as a generalization of string grammars, can be seen as a
powerful formalism for the specification of concurrent and distributed
systems, which properly extends Petri nets.  The idea is that the
state of a distributed system can be naturally represented (at a
suitable level of abstraction) as a graph, and local state
transformations can be expressed as production applications.

In this talk we first illustrate the basics of GTS's, pointing out the
features which make them more appropriate than ordinary Petri nets
when modelling distributed systems with a dinamically changing
topology (e.g., pi-calculus) and systems based on the shared-memory
model (e.g., Linda-like coordination languages, concurrent constraint
programs).

Then, focusing on the so-called double pushout (DPO) algebraic
approach to graph rewriting, we discuss the problem of providing GTS's
with a truly concurrent semantics. Generalizing some classical
approaches to the semantics of Petri nets, GTS's are endowed with
concurrent semantics based on (concatenable) processes and on a
Winskel's style unfolding construction, as well as with more abstract
semantics based on event structures and domains.

Finally we suggest how the proposed semantics can serve as a basis for
performing a formal verification activity on the modelled system.