Model Checking Graph Grammars
Arend Rensink · 2003
We sketch a setup in which transition systems are generated from graph grammars andsubsequently checked for properties expressed in a temporal logic on graphs. We envisage this as part of an approach where graph grammars are used to express the behavioural semantics ofobject-oriented programs, thus enabling automatic verification of those programs. This paper describes work in progress.