The dual equivalence of equations and coequations for automata

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 a state 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). 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.

This duality comes along with a coinduction proof principle,
phrased in terms of the new notion of equational bisimulation,
with which one can prove that a language belongs to a given variety.

This is joint work with Adolfo Ballester-Bolinches and
Enric Cosme-Llopez, Dept. of Mathematics, University of Valencia:

A. Ballester-Bolinches, E. Cosme-Llopez, J. Rutten.
The dual equivalence of equations and coequations for automata.
CWI Technical Report report FM-1403, 2014, pp. 1--30.
Available through http://homepages.cwi.nl/~janr/papers/