Weighted automata and quantitative logics

In automata theory, a classical result of Buchi states that the recognizable languages are precisely the ones definable by sentences of monadic second order logic. We will present a generalization of this result to the context of weighted automata. A weighted automaton is a classical nondeterministic automaton in which each transition carries a weight describing e.g. the resources used for its execution, the length of time needed, or its reliability. The behavior (language) of such a weighted automaton is a function associating to each word the weight of its execution. We develop syntax and semantics of a quantitative logic; the semantics counts `how often' a formula is true. Our main results show that if the weights are taken either in an arbitrary semiring or in an arbitrary bounded lattice, then the behaviors of weighted automata are precisely the functions definable by sentences of our quantitative logic. Buchi's result follows from either version by considering the classical Boolean algebra {0,1}.

Joint work with Paul Gastin (ENS Cachan) resp. Heiko Vogler (TU Dresden).