Document Open Access Logo

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

Authors Andrew Scoones , Mahsa Shirmohammadi , James Worrell

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.18.pdf
  • Filesize: 0.71 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Quantitative automata
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Verification by model checking
Keywords
  • Bilinear constraints
  • Existential theory of real closed fields
  • Diophantine approximation
  • Pareto curve

Metrics

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

Abstract

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.

Cite As Get BibTex

Andrew Scoones, Mahsa Shirmohammadi, and James Worrell. Reachability for Multi-Priced Timed Automata with Positive and Negative Rates. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.18

Author Details

Andrew Scoones
  • Department of Computer Science, University of Oxford, UK
Mahsa Shirmohammadi
  • CNRS, IRIF, Université of Paris Cité, France
James Worrell
  • Department of Computer Science, University of Oxford, UK

Funding

  • Scoones, Andrew: Supported by UKRI Frontier Research Grant EP/X033813/1.
  • Shirmohammadi, Mahsa: Supported by VeSyAM (ANR-22- CE48-0005).
  • Worrell, James: Supported by UKRI Frontier Research Grant EP/X033813/1.

References

  1. R. Alur and D. Dill. A theory of timed automata. TCS, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. In HSCC, volume 2034 of LNCS, pages 49-62. Springer, 2001. URL: https://doi.org/10.1007/3-540-45351-2_8.
  3. S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2006. Google Scholar
  4. Devendra B., Krishna S., and Trivedi A. On nonlinear prices in timed automata. In Proceedings of the The First Workshop on Verification and Validation of Cyber-Physical Systems, V2CPS@IFM, volume 232 of EPTCS, pages 65-78, 2016. URL: https://doi.org/10.4204/EPTCS.232.9.
  5. W. Banaszczyk, A. E. Litvak, A. Pajor, and S. J Szarek. The flatness theorem for nonsymmetric convex bodies via the local theory of banach spaces. Mathematics of operations research, 24(3):728-750, 1999. URL: https://doi.org/10.1287/MOOR.24.3.728.
  6. 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 HSCC, volume 2034 of LNCS, pages 147-161. Springer, 2001. URL: https://doi.org/10.1007/3-540-45351-2_15.
  7. 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. URL: https://doi.org/10.1007/S10703-007-0043-4.
  8. 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
  9. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey. Quantitative analysis of real-time systems using priced timed automata. Commun. ACM, 54(9):78-87, 2011. URL: https://doi.org/10.1145/1995376.1995396.
  10. T. Brihaye, V. Bruyère, and J.-F. Raskin. On model-checking timed automata with stopwatch observers. Inf. Comput., 204(3):408-433, 2006. URL: https://doi.org/10.1016/J.IC.2005.12.001.
  11. I. Diakonikolas and M. Yannakakis. Small approximate pareto sets for biobjective shortest paths and other problems. SIAM J. Comput., 39(4):1340-1371, 2009. URL: https://doi.org/10.1137/080724514.
  12. M Fränzle, M Shirmohammadi, M Swaminathan, and J Worrell. Costs and rewards in priced timed automata. Inf. Comput., 282:104656, 2022. URL: https://doi.org/10.1016/J.IC.2020.104656.
  13. M. Fränzle and M. Swaminathan. Revisiting decidability and optimum reachability for multi-priced timed automata. In The 7th International Conference on Formal Modelling and Analysis of Timed Systems, pages 149-163. Springer Verlag, September 2009. Google Scholar
  14. M. Grötschel, L. Lovász, and A. Schrijver. Geometric algorithms and combinatorial optimization, volume 2. Springer Science & Business Media, 2012. Google Scholar
  15. Q. Guilmant and J. Ouaknine. Inapproximability in weighted timed games. In Proceedings of CONCUR 24, volume 311 of LIPIcs, 2024. Google Scholar
  16. R. Hemmecke, M. Köppe, J. Lee, and R. Weismantel. Nonlinear integer programming. Springer, 2010. Google Scholar
  17. 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. URL: https://doi.org/10.1006/JCSS.1998.1581.
  18. R. Kannan and L. Lovász. Covering minima and lattice-point-free convex bodies. Annals of Mathematics, pages 577-602, 1988. Google Scholar
  19. L. Khachiyan and L. Porkolab. Integer optimization on convex semialgebraic sets. Discrete & Computational Geometry, 23:207-224, 2000. URL: https://doi.org/10.1007/PL00009496.
  20. 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 CAV, volume 2102 of LNCS, pages 493-505. Springer, 2001. URL: https://doi.org/10.1007/3-540-44585-4_47.
  21. K. G. Larsen and J. I. Rasmussen. Optimal reachability for multi-priced timed automata. TCS, 390(2-3):197-213, 2008. URL: https://doi.org/10.1016/J.TCS.2007.09.021.
  22. J. Ouaknine and J. Worrell. Revisiting digitization, robustness, and decidability for timed automata. In 18th IEEE Symposium on Logic in Computer Science (LICS, Proceedings, pages 198-207. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210059.
  23. L. Pottier. Minimal solutions of linear diophantine systems: bounds and algorithms. In International Conference on Rewriting Techniques and Applications, pages 162-173. Springer, 1991. Google Scholar
  24. M. Schaefer and D. Stefankovic. Fixed points, nash equilibria, and the existential theory of the reals. Theory Comput. Syst., 60(2):172-193, 2017. URL: https://doi.org/10.1007/S00224-015-9662-0.
  25. R. G. Tollund, N. S. Johansen, K. Ø. Nielsen, A. Torralba, and K. G. Larsen. Optimal infinite temporal planning: Cyclic plans for priced timed automata. In Proceedings of the Thirty-Fourth International Conference on Automated Planning and Scheduling, ICAPS, pages 588-596. AAAI Press, 2024. URL: https://doi.org/10.1609/ICAPS.V34I1.31521.
  26. Z. Zhang, B. Nielsen, K. G. Larsen, G. Nies, M. Stenger, and H. Hermanns. Pareto optimal reachability analysis for simple priced timed automata. In ICFEM, volume 10610 of LNCS, pages 481-495. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68690-5_29.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact