Completeness theorems for automata

Abstract

These notes present completeness results for varieties of products, state mappings and auxiliary variable constructions, for a (Mealy) automata-theoretic model of computation that generalizes the I/O automaton model of Lynch and Tuttle [Lyn88, LT87]. Conditions are examined under which these tools suffice to demonstrate that one specification implements another. The major theorem is a restatement of a completeness theorem due to Abadi and Lamport [AL88], translated from their (Moore) state machine model. The multivalued possibilities mappings of Lynch and Tuttle are used in place of the single-valued refinement mappings of Abadi and Lamport. A new kind of state mapping, prophecy mappings, is defined. Prophecy mappings are the time-reversal of possibilities mappings. This definition admits greater modularity in the proofs of Abadi and Lamport’s results. Additional results explore properties of products of automata, developing more fully ideas implicit in Abadi and Lamport’s work.