Automata and fixed point logic: A coalgebraic perspective

This paper generalizes existing connections between automata and logic to a coalgestraction level. Let F : Set Set be a standard functor 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 the two approaches are equivalent in expressive power. We prove that any coalgebraic fixed point formula can be transformed into an F-automaton that accepts precisely those pointed F-coalgebras in which the formula holds. And conversely, we prove that any F-automaton can be converted into an equivalent fixed point formula that characterizes the pointed F-coalgebras accepted by the automaton. Keywords coalgebra, automata, modal logic, fixed ...

• Type: Journal
• Year: 2006
• Where: IANDC
• Authors: Yde Venema
• Keywords: Coalgebraic Fixed Point, Fixed Point, IANDC 2006, Pointed F-coalgebras