Chatterjee, KrishnenduDoyen, LaurentHenzinger, Thomas A.2011-12-162011-12-162011-12-16201010.2168/LMCS-6(3:10)2010https://infoscience.epfl.ch/handle/20.500.14299/75089WOS:000282653500010Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages L that assign to each word w a real number L(w). In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the transition weights. The value of a word w is the supremum of the values of the runs over w. We study expressiveness and closure questions about these quantitative languages.Quantitative verificationWeighted automataExpressiveness and closure propertiesWeighted AutomataStochastic GamesLogicsComplexityPayofftext::journal::journal article::research article