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

Research output: Contribution to conference without publisher/journalPaper without publisher/journalResearchpeer-review

Abstract

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.
Original languageEnglish
Publication date2011
Number of pages9
Publication statusPublished - 2011
EventAnnual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - Lednice, Czech Republic
Duration: 14 Oct 201116 Oct 2011

Conference

ConferenceAnnual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Country/TerritoryCzech Republic
CityLednice
Period14/10/201116/10/2011

Bibliographical note

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

Fingerprint

Dive into the research topics of 'Optimal Infinite Runs in One-Clock Priced Timed Automata'. Together they form a unique fingerprint.

Cite this