Automata and Fixed Point Logic: a Coalgebraic Perspective
Yde Venema
Abstract:
This paper generalizes existing connections between automata and logic
to a coalgebraic level.
Let F be a standard endofunctor on Set that preserves weak pullbacks.
We introduce various notions of F-automata, devices that operate 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 A(P) which is
equivalent to P in the sense that A(P) accepts precisely those pointed
F-coalgebras in which P holds.