Proving Nonreachability by Modulo-Invariants. - Jörg Desel; Klaus-Peter Neuendorf; M.-D. Radola (Theor. Comput. Sci., 1996)