- Automata for Coalgebras: an approach using predicate liftings
- Lecture Notes in Computer Science
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
Universal Coalgebra provides the notion of a coalgebra as the natural mathematical generalization of state-based evolving systems such as (infinite) words, trees, and transition systems. We lift the theory of parity automata to this level of abstraction by introducing, for a set Λ of predicate liftings associated with a set functor T, the notion of a Λ-automata operating on coalgebras of type T. In a familiar way these automata correspond to extensions of coalgebraic modal logics with least and greatest fixpoint operators.
Our main technical contribution is a general bounded model property result: We provide a construction that transforms an arbitrary Λ-automaton \mathbbAA with nonempty language into a small pointed coalgebra (\mathbbS,s)(Ss) of type T that is recognized by \mathbbAA, and of size exponential in that of \mathbbAA. \mathbbSS is obtained in a uniform manner, on the basis of the winning strategy in our satisfiability game associated with \mathbbAA. On the basis of our proof we obtain a general upper bound for the complexity of the non-emptiness problem, under some mild conditions on Λ and T. Finally, relating our automata-theoretic approach to the tableaux-based one of Cîrstea et alii, we indicate how to obtain their results, based on the existence of a complete tableau calculus, in our framework.
- go to publisher's site
- Proceedings title: Automata, languages and programming: 37th International Colloquium, ICALP 2010, Bordeaux, France, July
6-10, 2010: proceedings. - Pt. 2
Place of publication: Berlin
Editors: S. Abramsky, C. Gavoille, C. Kirchner, F. Meyer auf der Heide, P.G. Spirakis