Tanszékcsoporti szeminárium

Quantitative models and quantitative analysis in Computer Science
are receiving increased attention. The goal of this talk is to
investigate quantitative automata and quantitative logics.
Weighted automata on finite words have already been investigated
in seminal work of Sch\"utzenberger (1961). They consist of classical
finite automata in which the transitions carry weights. These weights
may model, e.g., the cost, the consumption of resources, or the
reliability or probability of the successful execution of the
transitions. This concept soon developed a flourishing theory.

We investigate weighted automata and their relationship to weighted
logics. For this, we present syntax and semantics of a quantitative
logic; the semantics counts 'how often' a formula is true in a given
word. Our main result, extending the classical result of B\"uchi, shows
that if the weights are taken from an arbitrary semiring, then weighted
automata and a syntactically defined fragment of our weighted logic are
expressively equivalent. A corresponding result holds for infinite
words. Moreover, this extends to quantitative automata investigated by
Henzinger et al. with (non-semiring) average-type behaviors, or with
discounting or limit average objectives for infinite words.