Weighted automata and quantitative logics

Manfred Droste

(Universität Leipzig)

In automata theory, a classical result of Büchi 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 ressources used for its execution, the length of time needed, or its reliability. The behaviour (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 logics; the semantics counts 'how often' a formula is true. Our main result shows that if the weights are taken in an arbitrary commutative semiring, then the functions associated to weighted automata are precisely the ones definable by sentences of our quantitative logic.
(Joint work with Paul Gastin (Cachan)).
Tuesday 2nd October 2007, 14:00
Robert Recorde Room
Department of Computer Science