On the Supports of Recognizable Timed Series

Recently, the model of weighted timed automata has gained interest within the real-time community. In a previous work, we built a bridge to the theory of weighted automata and introduced a general model of weighted timed automata defined over a semiring and a family of cost functions. In this model, a weighted timed automaton recognizes a timed series, i.e., a function mapping to each timed word a weight taken from the semiring. Continuing in this spirit, the aim of this paper is to investigate the support and cut languages of recognizable timed series. We present results that lead to the decidability of weighted versions of classical decidability problems as e.g. the emptiness problem. Our results may also be used to check whether weighted timed systems satisfy specifications restricting the consumption of a resource.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Karin Quaas
• Keywords: Formal Methods, FORMATS 2009, Timed Series, Weighted Timed Automata, Weighted Timed Automaton