Coalgebraic automata theory: basic results

We generalize some of the central results in automata theory to the abstraction level of coalgebras and thus lay out the foundations of the theory of coalgebra automata. In particular, we prove the following results for any functor F that preserves weak pullbacks. We show that the class of recognizable languages of F-coalgebras is closed under taking unions, intersections, and projections. We also prove that if an F-automaton accepts some coalgebra it accepts a finite one of bounded size. Our main technical result concerns an explicit construction which transforms a given alternating F-automaton into an equivalent nondeterministic one, of bounded size.