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 , the notion of a Λ-automata operating on coalgebras of type . 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 with nonempty language into a small pointed coalgebra of type that is recognized by , and of size exponential in that of . is obtained in a uniform manner, on the basis of the winning strategy in our satisfiability game associated with . 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 . 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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Fontaine, G., Leal, R., & Venema, Y. (2010). Automata for coalgebras: An approach using predicate liftings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6199 LNCS, pp. 381–392). https://doi.org/10.1007/978-3-642-14162-1_32
Mendeley helps you to discover research relevant for your work.