Representation of a class of nondeterministic semiautomata by canonical words

It has been shown recently that deterministic semiautomata can be represented by canonical words and equivalences; that work was motivated by the trace-assertion method for specifying software modules. Here, we generalize these ideas to a class of nondeterministic semiautomata. A semiautomaton is settable if, for every state q, there exists a word wq such that q, and no other state, can be reached from some initial state by a path spelling wq. We extend many results from the deterministic case to settable nondeterministic semiautomata. Now each word has a number of canonical representatives. We show that a prefix-rewriting system exists for transforming any word to any of its representatives. If the set of canonical words is prefix-continuous (meaning that, if w and a prefix u of w are in the set, then all prefixes of w longer than u are also in the set), the rewriting system has no infinite derivations. Examples of specifications of nondeterministic modules are given.