Author(s):

Chatterjee, Krishnendu; Doyen, Laurent; Henzinger, Thomas A

Article Title: 
Expressiveness and closure properties for quantitative languages

Affiliation 
IST Austria 
Abstract: 
Weighted 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, limitaverage, or discountedsum 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. We first show that the set of words with value greater than a threshold can be omegaregular for deterministic limitaverage and discountedsum automata, while this set is always omegaregular when the threshold is isolated (i.e., some neighborhood around the threshold contains no word). In the latter case, we prove that the omegaregular language is robust against small perturbations of the transition weights. We next consider automata with transition weights 0 or 1 and show that they are as expressive as general weighted automata in the limitaverage case, but not in the discountedsum case. Third, for quantitative languages L1 and L2, we consider the operations max(L1, L2), min(L1, L2), and 1  L1, which generalize the boolean operations on languages, as well as the sum L1 + L2. We establish the closure properties of all classes of quantitative languages with respect to these four operations.

Keywords: 
quantitative verification; Weighted automata; Expressiveness and closure properties.

Journal Title:

Logical Methods in Computer Science

Volume: 
6

Issue 
3:10

ISSN:

18605974

Publisher:

International Federation of Computational Logic

Date Published:

20100830

Start Page: 
1

End Page:

23

Copyright Statement: 
CCBYND

URL: 

DOI: 
10.2168/LMCS6(3:10)2010

Notes: 
This research was supported in part by the Swiss National Science Foundation under the IndoSwiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), by the European projects Combest, Quasimodo, and Gasics, by the PAI program Moves funded by the Belgian Federal Government, and by the CFV (Federated Center in Verification) funded by the F.R.S. FNRS.

Open access: 
yes (OA journal) 