L. Aceto and A. Ingólfsdóttir, “Characteristic Formulae: From Automata to Logic”, BRICS, vol. 14, no. 2, Jan. 2007.