### Abstract

Language | Undefined |
---|---|

Article number | 10.1007/s10703-007-0043-4 |

Pages | 3-23 |

Number of pages | 21 |

Journal | Formal methods in system design |

Volume | 32 |

Issue number | 1 |

DOIs | |

State | Published - Feb 2008 |

### Keywords

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

### Cite this

*Formal methods in system design*,

*32*(1), 3-23. [10.1007/s10703-007-0043-4]. DOI: 10.1007/s10703-007-0043-4

}

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

Research output: Contribution to journal › Article

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 -