In: IEICE Trans. on Information and Systems, Vol. E82-D, No. 2, pages 339-347. 1999.
Abstract: Given two terms and their rewriting rules, an unreachability problem proves the non-existence of a reduction sequence from one term to another. This paper formalizes a method for solving unreachability problems by abstraction; i.e., reducing an original concrete unreachability problem to a simpler abstract unreachability problem to prove the unreachability of the original concrete problem if the abstract unreachability is proved. The class of rewriting systems discussed in this paper is called beta rewriting systems. The class of beta rewriting systems includes very important systems such as semi-Thue systems and Petri Nets. Abstract rewriting systems are also a subclass of beta rewriting systems. A beta rewriting system is defined on axiomatically formulated base structures, called beta structures, which are used to formalize the concepts of `contexts' and `replacement,' which are common to many rewritten objects. Each domain underlying semi-Thue systems, Petri Nets, and other rewriting systems are formalized by a beta structure. A concept of homomorphisms from a beta structure (a concrete domain) to a beta structure (an abstract domain) is introduced. A homomorphism theorem (Theorem 1) is established for beta rewriting systems, which states that concrete reachability implies abstract reachability. An unreachability theorem (Corollary 1) is also proved for beta rewriting systems. It is the contraposition of the homomorphism theorem, i.e., it says that abstract unreachability implies concrete unreachability. The unreachability theorem is used to solve two unreachability problems: a coffee bean puzzle and a checker board puzzle.
Keywords: Petri nets, beta rewriting system, homomorphism theorem, unreachability.