Graph transformation systems, Petri nets and Semilinear Sets: Checking for the Absence of Forbidden Paths in Graphs

We introduce an analysis method that checks for the absence of (Euler) paths or cycles in the set of graphs reachable from a start graph via graph transformation rules. This technique is based on the approximation of graph transformation systems by Petri nets and on semilinear sets of markings. An important application is deadlock analysis in distributed systems.