Optimal infinite scheduling for multi-priced timed automata |
| |
Authors: | Patricia Bouyer Ed Brinksma Kim G Larsen |
| |
Affiliation: | (1) LSV, CNRS & ENS de Cachan, UMR 8643, Cachan Cedex, France;(2) Department of Computer Science, University of Twente, Enschede, The Netherlands;(3) BRICS, Aalborg University, Aalborg, Denmark |
| |
Abstract: | This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover
a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes
both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite
behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such
double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles
in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a
powerful abstraction technique of which we show that it preserves optimal schedules.
This work has been mostly done while visiting CISS at Aalborg University in Denmark and has been supported by CISS and by
ACI Cortos, a program of the French Ministry of Research. |
| |
Keywords: | Priced timed automata Optimal mean-payoff |
本文献已被 SpringerLink 等数据库收录! |
|