Representation of semiautomata by canonical words and equivalences, Part II: Applications to the specification of software modules

Abstract. We study a novel representation of semiautomata, which is motivated by the method of trace-assertion specications of software modules. Each state of the semiautomaton is represented by an arbitrary word, the canonical word leading to that state. The transitions of the semiautomaton give rise to a right congruence, the state-equivalence, on the set of input words of the semiautomaton: two words are state-equivalent if and only if they lead to the same state. We present a simple algorithm for nding a set of generators for state-equivalence. Directly from this set of generators, we construct a con uent rewriting system which permits us to transform any word to its canonical representative. In general, the rewriting system may allow in nite derivations. To address this issue, we impose the condition of prex-continuity on the set of canonical words. A set is prex-continuous if whenever a word w and a pre x u of w are in the set, then all the prexes of w longer than u are also in the set. Pre x-continuous sets include prex codes and prex-closed sets as special cases. We prove that the rewriting system is Noetherian if and only if the set of canonical words is prex-continuous. Furthermore, if the set of canonical words is prex-continuous, then the set of rewriting rules is irredundant. We show that each prex-continuous canonical set corresponds to a spanning forest of the semiautomaton.