Regular languages have proved useful for the symbolic
state exploration of infinite state systems. They can be
used to represent infinite sets of system configurations; the
transitional semantics of the system consequently can be modeled by
finite-state transducers. A standard problem encountered when doing
symbolic state exploration for infinite state systems is how to explore
all states in a finite amount of time.
When representing the one-step transition relation of a system by a
finite-state transducer $\T$, this problem boils down to finding an
appropriate
finite-state representation $\Tmany$ for its transitive
closure.
In this paper we give a partial algorithm to compute a finite-state
transducer $\Tmany$ for a general class of transducers,
including transducers that are not length-preserving. The
construction builds a quotient of an underlying infinite-state
transducer $\Tmanyinfinite$, using a novel behavioural equivalence
that is based \emph{past} and \emph{future} bisimulations computed
on finite approximations of $\Tmanyinfinite$. The extrapolation to
$\Tmanyinfinite$ of these finite bisimulations capitalizes on the
structure of the states of $\Tmanyinfinite$, which are strings of
states of $\T$. We show how this extrapolation may be rephrased as a
problem of detecting \emph{confluence} properties of rewrite systems
that represent the bisimulations. Thus, we can draw upon techniques
that have been developed in the area of rewriting.
As in general, $\Tmanyinfinite$ is not representable by a finite-state
transducer, the construction may not terminate. Nevertheless our
implementation is able to calculate the transitive closure on
examples investigated by related symbolic techniques in the literature.
