Automata and Fixed Point Logics for Coalgebras

It is the aim of this paper to generalize existing connections between automata and logic to a more general, coalgebraic level.Let F:Set→Set be a standard functor that preserves weak pullbacks. We introduce the notion of an F-automaton, a device that operates on pointed F-coalgebras; the criterion under which such an automaton accepts or rejects a pointed coalgebra is formulated in terms of an infinite two-player graph game.We also introduce a language of coalgebraic fixed point logic for F-coalgebras, and we provide a game semantics for this language. Finally we show that any formula p of the language can be transformed into an F-automaton Ap which is equivalent to p in the sense that Ap accepts precisely those pointed F-coalgebras in which p holds