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

    48 Citations (Scopus)
    44 Downloads (Pure)

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

    Keywords

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

    Cite this

    Alur, R. (Ed.), Bouyer, P., Pappas, G. J. (Ed.), Brinksma, H., & Larsen, K. G. (2008). Optimal infinite scheduling for multi-priced timed automata. Formal methods in system design, 32(1), 3-23. [10.1007/s10703-007-0043-4]. https://doi.org/10.1007/s10703-007-0043-4
    Alur, R (Editor) ; Bouyer, Patricia ; Pappas, G.J. (Editor) ; Brinksma, Hendrik ; Larsen, K.G. / Optimal infinite scheduling for multi-priced timed automata. In: Formal methods in system design. 2008 ; Vol. 32, No. 1. pp. 3-23.
    @article{6405403592a445529a377aa02cfb0572,
    title = "Optimal infinite scheduling for multi-priced timed automata",
    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.",
    keywords = "Priced timed automata · Optimal mean-payoff, EWI-13260, IR-64936, METIS-221483",
    author = "R Alur and Patricia Bouyer and G.J. Pappas and Hendrik Brinksma and K.G. Larsen",
    note = "Selected papers from the Seventh International Conference on Hybrid Systems: Computation and Control (HSCC 2004)",
    year = "2008",
    month = "2",
    doi = "10.1007/s10703-007-0043-4",
    language = "Undefined",
    volume = "32",
    pages = "3--23",
    journal = "Formal methods in system design",
    issn = "0925-9856",
    publisher = "Springer",
    number = "1",

    }

    Alur, R (ed.), Bouyer, P, Pappas, GJ (ed.), Brinksma, H & Larsen, KG 2008, 'Optimal infinite scheduling for multi-priced timed automata', Formal methods in system design, vol. 32, no. 1, 10.1007/s10703-007-0043-4, pp. 3-23. https://doi.org/10.1007/s10703-007-0043-4

    Optimal infinite scheduling for multi-priced timed automata. / Alur, R (Editor); Bouyer, Patricia; Pappas, G.J. (Editor); Brinksma, Hendrik; Larsen, K.G.

    In: Formal methods in system design, Vol. 32, No. 1, 10.1007/s10703-007-0043-4, 02.2008, p. 3-23.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Optimal infinite scheduling for multi-priced timed automata

    AU - Bouyer, Patricia

    AU - Brinksma, Hendrik

    AU - Larsen, K.G.

    A2 - Alur, R

    A2 - Pappas, G.J.

    N1 - Selected papers from the Seventh International Conference on Hybrid Systems: Computation and Control (HSCC 2004)

    PY - 2008/2

    Y1 - 2008/2

    N2 - 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.

    AB - 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.

    KW - Priced timed automata · Optimal mean-payoff

    KW - EWI-13260

    KW - IR-64936

    KW - METIS-221483

    U2 - 10.1007/s10703-007-0043-4

    DO - 10.1007/s10703-007-0043-4

    M3 - Article

    VL - 32

    SP - 3

    EP - 23

    JO - Formal methods in system design

    JF - Formal methods in system design

    SN - 0925-9856

    IS - 1

    M1 - 10.1007/s10703-007-0043-4

    ER -

    Alur R, (ed.), Bouyer P, Pappas GJ, (ed.), Brinksma H, Larsen KG. Optimal infinite scheduling for multi-priced timed automata. Formal methods in system design. 2008 Feb;32(1):3-23. 10.1007/s10703-007-0043-4. https://doi.org/10.1007/s10703-007-0043-4