Document Open Access Logo

Costs and Rewards in Priced Timed Automata

Authors Martin Fränzle, Mahsa Shirmohammadi, Mani Swaminathan, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.125.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Martin Fränzle
  • Department of Computing Science, University of Oldenburg, Germany
Mahsa Shirmohammadi
  • CNRS & LIS, France
Mani Swaminathan
  • Department of Computing Science, University of Oldenburg, Germany
James Worrell
  • Department of Computer Science, University of Oxford, UK

Cite AsGet BibTex

Martin Fränzle, Mahsa Shirmohammadi, Mani Swaminathan, and James Worrell. Costs and Rewards in Priced Timed Automata. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 125:1-125:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ICALP.2018.125

Abstract

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10^{th} Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Priced Timed Automata
  • Pareto Domination
  • Diophantine Equations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. R. Alur and D. Dill. A theory of timed automata. TCS, 126(2):183-235, 1994. Google Scholar
  2. R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. In M.-D. Di Benedetto and A. S-Vincentelli, editors, HSCC, volume 2034 of LNCS, pages 49-62. Springer, 2001. Google Scholar
  3. G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson, J. Romijn, and F. W. Vaandrager. Minimum-cost reachability for priced timed automata. In M.-D. Di Benedetto and A. S-Vincentelli, editors, HSCC, volume 2034 of LNCS, pages 147-161. Springer, 2001. Google Scholar
  4. P. Bouyer, T. Brihaye, V. Bruyère, and J.-F. Raskin. On the optimal reachability problem of weighted timed automata. Formal Methods in System Design, 31(2):135-175, 2007. Google Scholar
  5. P. Bouyer, E. Brinksma, and K. G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design, 32(1):3-23, 2008. Google Scholar
  6. P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and J. Srba. Infinite runs in weighted timed automata with energy constraints. In F. Cassez and C. Jard, editors, FORMATS, volume 5215 of LNCS, pages 33-47. Springer, 2008. Google Scholar
  7. P. Bouyer, K. G. Larsen, and N. Markey. Model checking one-clock priced timed automata. Logical Methods in Computer Science, 4:1-28, 2008. Google Scholar
  8. T. Brihaye, V. Bruyère, and J.-F. Raskin. On model-checking timed automata with stopwatch observers. Inf. Comput., 204(3):408-433, 2006. Google Scholar
  9. I. Diakonikolas and M. Yannakakis. Small approximate pareto sets for biobjective shortest paths and other problems. SIAM J. Comput., 39(4):1340-1371, 2009. Google Scholar
  10. M. Fränzle, M. Shirmohammadi, M. Swaminathan, and J. Worrell. Costs and rewards in priced timed automata. CoRR, 2018. URL: https://arxiv.org/abs/1803.01914.
  11. M. Fränzle and M. Swaminathan. Revisiting decidability and optimum reachability for multi-priced timed automata. In J. Ouaknine and F. W. Vaandrager, editors, FORMATS, volume 5813 of LNCS, pages 149-163. Springer, 2009. Google Scholar
  12. F. Grunewald and D. Segal. On the integer solutions of quadratic equations. Journal für die reine und angewandte Mathematik, 569:13-45, 2004. Google Scholar
  13. C. Haase and S. Halfon. Integer vector addition systems with states. In J. Ouaknine, I. Potapov, and J. Worrell, editors, RP, volume 8762 of LNCS, pages 112-124. Springer, 2014. Google Scholar
  14. T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? J. Comput. Syst. Sci., 57(1):94-124, 1998. Google Scholar
  15. J. P. Jones. Undecidable diophantine equations. Bull. Amer. Math. Soc., 3:859-862, 1980. Google Scholar
  16. K. G. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn. As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In G. Berry, H. Comon, and A. Finkel, editors, CAV, volume 2102 of LNCS, pages 493-505. Springer, 2001. Google Scholar
  17. K. G. Larsen and J. I. Rasmussen. Optimal reachability for multi-priced timed automata. TCS, 390(2-3):197-213, 2008. Google Scholar
  18. V. Perevoshchikov. Multi-weighted automata models and quantitative logics. PhD thesis, University of Leipzig, 2015. Google Scholar
  19. K. Quaas. Kleene-Schützenberger and Büchi theorems for weighted timed automata. PhD thesis, University of Leipzig, 2010. Google Scholar
  20. A. W. To. Parikh images of regular languages: Complexity and applications. CoRR, 2010. URL: http://arxiv.org/abs/1002.1464.
  21. T. Zaslavsky. Signed graphs. Discrete Applied Mathematics, 4(1):47-74, 1982. Google Scholar
  22. Z. Zhang, B. Nielsen, K. G. Larsen, G. Nies, M. Stenger, and H. Hermanns. Pareto optimal reachability analysis for simple priced timed automata. In Z. Duan and L. Ong, editors, ICFEM, volume 10610 of LNCS, pages 481-495. Springer, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact