Optimal infinite scheduling for multi-priced timed automata

R Alur (Editor), Patricia Bouyer, G.J. Pappas (Editor), Hendrik Brinksma, K.G. Larsen

    Research output: Contribution to journalArticleAcademicpeer-review

    49 Citations (Scopus)
    60 Downloads (Pure)


    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.
    Original languageUndefined
    Article number10.1007/s10703-007-0043-4
    Pages (from-to)3-23
    Number of pages21
    JournalFormal methods in system design
    Issue number1
    Publication statusPublished - Feb 2008


    • Priced timed automata · Optimal mean-payoff
    • EWI-13260
    • IR-64936
    • METIS-221483

    Cite this