## Kleene-Schützenberger and Büchi Theorems for Weighted Timed AutomataIn 1994, Alur and Dill introduced timed automata as a simple mathematical model for modelling the behaviour of real-time systems. In this thesis, we extend timed automata with weights. More detailed, we equip both the states and transitions of a timed automaton with weights taken from an appropriate mathematical structure. The weight of a transition determines the weight for taking this transition, and the weight of a state determines the weight for letting time elapse in this state. Since the weight for staying in a state depends on time, this model, called weighted timed automata, has many interesting applications, for instance, in operations research and scheduling. We give characterizations for the behaviours of weighted timed automata in terms of rational expressions and logical formulas. These formalisms are useful for the specification of real-time systems with continuous resource consumption. We further investigate the relation between the behaviours of weighted timed automata and timed automata. Finally, we present important decidability results for weighted timed automata. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 | |

Weighted Timed Automata | 15 |

A KleeneSchutzenberger Theorem for Weighted Timed Automata | 27 |

A Buchi Theorem for Weighted Timed Automata | 51 |

Supports and Timed Cut Languages | 81 |

Conclusion and Future Work | 103 |

### Common terms and phrases

addition and multiplication Alur assume atomic formulas B¨uchi theorem behaviour bounded variability Cauchy product classical clock run clock valuations clock variables construction corresponding cut languages decidable deﬁne deﬁnition denote diﬀerence dom(w edge editors equivalent ewt(e ewt(ei family of linear family of step ﬁeld ﬁrst ﬁrst-order first-order variable formal power series Hadamard product Hence idempotent in(l in(Z inﬁnite IR>o Iwt(Z JF-rational Kleene star Kleene theorem linear functions LNCS min-plus-semiring model checking model of weighted monoid MSO logic n-clock series n-clock word non-interfering obtain out(Z pointwise product quantiﬁer real numbers recognizable timed series region automaton relative distance logic restricted running weight rwt(r satisﬁes semantics semiring Springer step functions syntactically unambiguous TA-recognizable timed languages Theorem 5.9 theory of weighted transition unambiguously TA-recognizable Universal Quantification unweighted weight functions weighted ﬁnite automata weighted timed automaton weighted version WFA-recognizable series zero-sum free