Optimal Infinite Runs in One-Clock Priced Timed Automata

Alexandre David, Daniel Ejsing-Duun, Lisa Fontani, Kim Guldstrand Larsen, Vasile Popescu, Jacob Haubach Smedegård

Publikation: Konferencebidrag uden forlag/tidsskriftPaper uden forlag/tidsskriftForskningpeer review

Resumé

We address the problem of finding an infinite run with the
optimal cost-time ratio in a one-clock priced timed automaton and pro-
vide an algorithmic solution. Through refinements of the quotient graph
obtained by strong time-abstracting bisimulation partitioning, we con-
struct a graph with time and costs as weights and prove that the min-
imum ratio properties remain unaltered, allowing algorithms for finite
weighted graphs to be applied. The resulting algorithm has an overall
time complexity of O((|Q| · (|T | + |Q|))6 ), |Q| being the number of lo-
cations and |T | the number of transitions of the one-clock priced timed
automaton.
OriginalsprogEngelsk
Publikationsdato2011
Antal sider9
StatusUdgivet - 2011
BegivenhedAnnual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - Lednice, Tjekkiet
Varighed: 14 okt. 201116 okt. 2011

Konference

KonferenceAnnual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
LandTjekkiet
ByLednice
Periode14/10/201116/10/2011

Fingerprint

Timed Automata
Bisimulation
Costs
Graph in graph theory
Partitioning
Quotient
Refinement

Citer dette

David, A., Ejsing-Duun, D., Fontani, L., Larsen, K. G., Popescu, V., & Haubach Smedegård, J. (2011). Optimal Infinite Runs in One-Clock Priced Timed Automata. Afhandling præsenteret på Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Lednice, Tjekkiet.
David, Alexandre ; Ejsing-Duun, Daniel ; Fontani, Lisa ; Larsen, Kim Guldstrand ; Popescu, Vasile ; Haubach Smedegård, Jacob. / Optimal Infinite Runs in One-Clock Priced Timed Automata. Afhandling præsenteret på Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Lednice, Tjekkiet.9 s.
@conference{dac30f24832844de9bad00f2fc261b6a,
title = "Optimal Infinite Runs in One-Clock Priced Timed Automata",
abstract = "We address the problem of finding an infinite run with theoptimal cost-time ratio in a one-clock priced timed automaton and pro-vide an algorithmic solution. Through refinements of the quotient graphobtained by strong time-abstracting bisimulation partitioning, we con-struct a graph with time and costs as weights and prove that the min-imum ratio properties remain unaltered, allowing algorithms for finiteweighted graphs to be applied. The resulting algorithm has an overalltime complexity of O((|Q| · (|T | + |Q|))6 ), |Q| being the number of lo-cations and |T | the number of transitions of the one-clock priced timedautomaton.",
author = "Alexandre David and Daniel Ejsing-Duun and Lisa Fontani and Larsen, {Kim Guldstrand} and Vasile Popescu and {Haubach Smedeg{\aa}rd}, Jacob",
note = "Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS); null ; Conference date: 14-10-2011 Through 16-10-2011",
year = "2011",
language = "English",

}

David, A, Ejsing-Duun, D, Fontani, L, Larsen, KG, Popescu, V & Haubach Smedegård, J 2011, 'Optimal Infinite Runs in One-Clock Priced Timed Automata', Paper fremlagt ved Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Lednice, Tjekkiet, 14/10/2011 - 16/10/2011.

Optimal Infinite Runs in One-Clock Priced Timed Automata. / David, Alexandre; Ejsing-Duun, Daniel; Fontani, Lisa; Larsen, Kim Guldstrand; Popescu, Vasile; Haubach Smedegård, Jacob.

2011. Afhandling præsenteret på Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Lednice, Tjekkiet.

Publikation: Konferencebidrag uden forlag/tidsskriftPaper uden forlag/tidsskriftForskningpeer review

TY - CONF

T1 - Optimal Infinite Runs in One-Clock Priced Timed Automata

AU - David, Alexandre

AU - Ejsing-Duun, Daniel

AU - Fontani, Lisa

AU - Larsen, Kim Guldstrand

AU - Popescu, Vasile

AU - Haubach Smedegård, Jacob

N1 - Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS)

PY - 2011

Y1 - 2011

N2 - We address the problem of finding an infinite run with theoptimal cost-time ratio in a one-clock priced timed automaton and pro-vide an algorithmic solution. Through refinements of the quotient graphobtained by strong time-abstracting bisimulation partitioning, we con-struct a graph with time and costs as weights and prove that the min-imum ratio properties remain unaltered, allowing algorithms for finiteweighted graphs to be applied. The resulting algorithm has an overalltime complexity of O((|Q| · (|T | + |Q|))6 ), |Q| being the number of lo-cations and |T | the number of transitions of the one-clock priced timedautomaton.

AB - We address the problem of finding an infinite run with theoptimal cost-time ratio in a one-clock priced timed automaton and pro-vide an algorithmic solution. Through refinements of the quotient graphobtained by strong time-abstracting bisimulation partitioning, we con-struct a graph with time and costs as weights and prove that the min-imum ratio properties remain unaltered, allowing algorithms for finiteweighted graphs to be applied. The resulting algorithm has an overalltime complexity of O((|Q| · (|T | + |Q|))6 ), |Q| being the number of lo-cations and |T | the number of transitions of the one-clock priced timedautomaton.

M3 - Paper without publisher/journal

ER -

David A, Ejsing-Duun D, Fontani L, Larsen KG, Popescu V, Haubach Smedegård J. Optimal Infinite Runs in One-Clock Priced Timed Automata. 2011. Afhandling præsenteret på Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Lednice, Tjekkiet.