Because of the isomorphism (X x A) -> X = X -> (A -> X), the transition structure t: X -> (A -> X) of a deterministic automaton with state set X and with inputs from an alphabet A can be viewed both as an algebra and as a coalgebra. Here we will use this algebra-coalgebra duality of automata as a common perspective for the study of equations and coequations. Equations are sets of pairs of words (v,w) that are satisfied by a state x in X if they lead to the same state: x_v=x_w. Dually, coequations are sets of languages and are satisfied by x if the language accepted by x belongs to that set. For every automaton (X, t), we define two new automata: free(X, t) and cofree(X, t) that represent, respectively, the greatest set of equations and the smallest set of coequations satisfied by (X, t) . Both constructions are shown to be functorial, that is, they act also on automaton homomorphisms. The automaton free(X, t) is isomorphic to the so-called transition monoid of (X, t) , and thereby, cofree(X, t) can be seen as its dual. Our main result is that the restrictions of free and cofree to, respectively, varieties of languages and to quotients A*/C of A* with respect to a congruence relation C, form a dual equivalence. In the present context, varieties of languages are sets of -- not necessarily regular -- languages that are complete atomic Boolean algebras closed under left and right language derivatives.
, ,
Formal methods [FM]
Computer Security

Ballester-Bolinches, A., Cosme-Llopez, E., & Rutten, J. (2014). The dual equivalence of equations and coequations for automata. Formal methods [FM]. CWI.