Optimal infinite scheduling for multi-priced timed automata

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

  • 44 Citations

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
StatePublished - Feb 2008

Fingerprint

Costs

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]. DOI: 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, Vol. 32, No. 1, 10.1007/s10703-007-0043-4, 02.2008, p. 3-23.

Research output: Scientific - peer-reviewArticle

@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",
volume = "32",
pages = "3--23",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer Netherlands",
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. DOI: 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: Scientific - peer-reviewArticle

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

T2 - 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. Available from, DOI: 10.1007/s10703-007-0043-4