"Proving Nonreachability by Modulo-Invariants."

Jörg Desel, Klaus-Peter Neuendorf, M.-D. Radola (1996)
a service of Schloss Dagstuhl - Leibniz Center for Informatics