  We introduce a novel technique for checking reachability in Petri nets that
relies on a recently introduced compositional algebra of nets. We prove that
the technique is correct, and discuss our implementation. We report promising
experimental results on some well-known examples.
