The dual equivalence of equations and coequations for automata (Q498397)

This article investigates deterministic (potentially infinite-state) automata from a category-theoretic perspective. The basis of each automaton, its transition system, is an algebra and a co-algebra. Adding an initial state preserves the algebra structure, but adding a set of final states only preserves the co-algebra structure. In the following, let \(A = (Q, \Sigma, \delta)\) be a transition system with (potentially infinite) sets \(Q\) and \(\Sigma\) and transition function \(\delta : Q \times \Sigma \to Q\). Each choice \(q \in Q\) of an initial state determines a unique homomorphism \(h_q : \Sigma^* \to Q\), namely the one that given an input \(w \in \Sigma^*\) assigns the state reached after reading \(w\) starting from \(q\) in the transition system \(A\). A set \(E\) of equations for \(A\) is defined to be a bisimulation equivalence \(E\) on \(\Sigma^*\) (i.e., an equivalence such that for every \((v, w) \in E\) also \((v\sigma, w\sigma) \in E\) for all \(\sigma \in \Sigma\)) such that \(h_q(v) = h_q(w)\) for all \((v, w) \in E\) and \(q \in Q\). In other words, if the words \(v\) and \(w\) are in relation, then no matter at which initial state we start we need to reach the same state processing \(v\) and \(w\). The transition structure \(\operatorname{free}(A)\) is the product of the automata \((A_q)_{q \in Q}\), where \(A_q\) is the transition structure \(A\) together with the initial state \(q\), factored by the kernel \(K\) of its reachability map. It is demonstrated that the kernel \(K\) is the largest set of equations for \(A\). Similarly, a set of co-equations is a subautomaton of the automaton of right languages such that the right language of each state \(q \in Q\) is contained for each choice of final states \(F \subseteq Q\). A co-product construction yields the automaton \(\operatorname{cofree}(A)\) representing the smallest set of co-equations for \(A\). Both constructions are actually functorial. Furthermore it is demonstrated that certain natural restrictions of \(\operatorname{free}(A)\) and \(\operatorname{cofree}(A)\) form a dual equivalence, and as a consequence a variant of Eilenberg's variety theorem is obtained. Although the paper uses category theory, the paper remains accessible to non-experts in category theory. All notions are carefully explained and should be understandable to graduate students of mathematics or theoretical computer science. Examples are provided for all major constructions and they illustrate the notions well. The constructions actually mirror well-known ones, like the construction of the syntactic monoid, so prior exposure to algebraic automata theory will help the reader.