*For the most recent entries see the
Petri Nets Newsletter.*

## Unreachability proofs for beta rewriting systems by homomorphisms.

Akama, K.;
Shigeta, Y.;
Miyamoto, E.
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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*