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

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 language | English |
---|---|

Publication date | 2011 |

Number of pages | 9 |

Publication status | Published - 2011 |

Event | Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - Lednice, Czech Republic Duration: 14 Oct 2011 → 16 Oct 2011 |

### Conference

Conference | Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science |
---|---|

Country | Czech Republic |

City | Lednice |

Period | 14/10/2011 → 16/10/2011 |