Coalgebra automata were invented by Yde Venema and first published on in his paper "Automata and Fixed Point Logics: A Coalgebraic Approach". Their purpose is two-fold. On the one hand, coalgebra automata provide a suitable means to study properties of automata for a large class of input types, comprising words, trees, and graphs. On the other hand coalgebra automata introduce fixed point operators in Moss' coalgebraic logic. The latter reflects the insight that states in coalgebra automata correspond to formulae of (some) coalgebraic logic, in the sense that an automaton accepts a point in a coalgebra iff that point satisfies the corresponding formula. This correspondence has been exploited in the case of trees by Michael Rabin in his decidability result for monadic second-order logic for binary trees (S2S).

This page is under construction. Please notify me ( email(at)christiankissig.de ) of any developments I have been missing.

Results

• Coalgebra automata are effectively closed under union and intersection, existential and universal projection, and under complementation
• The emptiness problem is effectively decidable for coalgebra automata
• Non-deterministic and alternating automata are effectively mutually translatable

Remark: by effectively we mean, that there is an explicit algorithmic description of the translation or decision procedure. Furthermore there are complexity results.

Bibliography (selected for conciseness and accessibility)

• C Kupke, Y Venema, Coalgebraic Automata Theory: Basic Results, Logical Methods in Computer Science, to appear
• Y Venema, Automata and Fixed Point Logics: A Coalgebraic Approach, Information and Computation 2006
• C Kissig, Y Venema, Complementation of Coalgebra Automata, CALCO 2009
• C Kissig, Satisfiability of S2S, Master of Logic Thesis, 2007