In: Proceedings of CONCUR 2004 - Concurrency Theory: 15th International Conference, London, UK, August 31 - September 3, 2004, pages 83-98. Volume 3170 of Lecture Notes in Computer Science / Philippa Gardner, Nobuko Yoshida (Eds.) --- Springer-Verlag, September 2004.
Abstract: We propose a framework where behavioural properties of finite-state systems modelled as graph transformation systems can be expressed and verified. The technique is based on the unfolding semantics and it generalises McMillan's complete prefix approach, originally developed for Petri nets, to graph transformation systems. It allows to check properties of the graphs reachable in the system, expressed in a monadic second order logic.