CONCUR 2004 START ConferenceManager    

Verifying Finite-State Graph Grammars: an Unfolding-Based Approach

Paolo Baldan, Andrea Corradini, Barbara Koenig

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


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.

START Conference Manager (V2.47.4)