In many applications we need to consider input and output as streams of symbols, with some desired relation between the input stream and the output stream. The most basic description for such systems, the one that we explore in this work, is when the domains are (possibly infinite) sets of finite words over finite alphabets, and the given relation is a regular language, given as a deterministic finite automaton (DFA), over the product alphabet of the input and output domains. The setting that we consider in this paper is of automatic relations, which are relations that are described by automata as defined below. Automatic relations provide a context for a rich theory of automatic structures, cf. [1]}, [2]}, with a solvable decision for first-order logic. We follow here the convention in regular model checking, cf. [3]}, where length-preserving automatic relations, with input and output symbols interleaved, are used as input/output specifications for each step of reactive systems. (Thus, unlike the definitions in [1]}, [2]}, we do not allow padding.)
