Model checking is increasingly popular for hardware and, more recently, software verification.
In this paper we describe two different approaches to extend the benefits of model
checking to systems whose behavior is specified by graph transformation systems. One
approach is to encode the graphs into the fixed state vectors and the transformation
rules into guarded commands that modify these state vectors appropriately to enjoy
all the benefits of the years of experience incorporated in existing model checking
tools. The other approach is to simulate the graph production rules directly and build
the state space directly from the resultant graphs and derivations. This avoids the
preprocessing phase, and makes additional abstraction techniques available to handle
symmetries and dynamic allocation. In this paper we compare these approaches on the
basis of three case studies elaborated in both of them, and we evaluate the results.
Our conclusion is that the first approach outperforms the second if the dynamic and/or
symmetric nature of the problem under analysis is limited, while the second shows
its superiority for inherently dynamic and symmetric problems.