Skip to main content
Department of Information Technology


During the last years, weighted timed automata (WTA) have received much interest
in the real-time community. Weighted timed automata form an extension of timed
automata and allow us to assign weights (costs) to both locations and edges.
This model, introduced by Alur et al. (2001) and Behrmann et al. (2001),
permits the treatment of continuous consumption of resources and has led to
much research on scheduling problems, optimal reachability and model checking.
Also, several authors have derived Kleene-type characterizations of (unweighted)
timed automata and their accepted timed languages.The goal of this paper is to
provide a characterization of the possible behaviours of WTA by rational power
series.We define WTA with weights taken in an arbitrary semiring, resulting in a model
that subsumes several WTA concepts of the literature.For our main result, we combine
the methods of Sch\"utzenberger, a recent approach for a Kleene-type theorem for
unweighted timed automata by Bouyer and Petit as well as new techniques.
Our main result also implies Kleene-type theorems for several subclasses of WTA
investigated before, e.g., for weighted finite automata, timed automata and
timed automata with stopwatch observers.

Updated  2008-03-17 14:01:10 by Lisa Kaati.