Towards model checking graph grammars
Arend Rensink · 2003
We sketch a setup in which transition systems are generated from graph grammars and subsequently 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 of object-oriented programs, thus enabling automatic verification of those programs.