Document Open Access Logo

A Zone-Based Algorithm for Timed Parity Games

Authors Gilles Geeraerts , Frédéric Herbreteau , Jean-François Raskin , Alexis Reynouard

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.33.pdf
  • Filesize: 1.1 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
Keywords
  • Timed Parity Games
  • Realtime Controller Synthesis

Metrics

Abstract

This paper revisits timed games by building upon the semantics introduced in "The Element of Surprise in Timed Games" [Luca de Alfaro et al., 2003]. We introduce some modifications to this semantics for two primary reasons: firstly, we recognize instances where the original semantics appears counterintuitive in the context of controller synthesis; secondly, we present methods to develop efficient zone-based algorithms. Our algorithm successfully addresses timed parity games, and we have implemented it using UPPAAL’s zone library. This prototype effectively demonstrates the feasibility of a zone-based algorithm for parity objectives and a rich semantics for timed interactions between the players.

Cite As Get BibTex

Gilles Geeraerts, Frédéric Herbreteau, Jean-François Raskin, and Alexis Reynouard. A Zone-Based Algorithm for Timed Parity Games. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.33

Author Details

Gilles Geeraerts
  • Université libre de Bruxelles, Belgium
Frédéric Herbreteau
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, 33400 Talence, France
Jean-François Raskin
  • Université libre de Bruxelles, Belgium
Alexis Reynouard
  • Université libre de Bruxelles, Belgium

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic controller synthesis for discrete and timed systems. In Panos J. Antsaklis, Wolf Kohn, Anil Nerode, and Shankar Sastry, editors, Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October 1994, volume 999 of Lecture Notes in Computer Science, pages 1-20. Springer, 1994. URL: https://doi.org/10.1007/3-540-60472-3_1.
  3. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 311-324. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CONCUR.2015.311.
  4. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Paul Pettersson and Wang Yi, editors, Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, volume 3829 of Lecture Notes in Computer Science, pages 49-64. Springer, 2005. URL: https://doi.org/10.1007/11603009_5.
  5. Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-François Raskin. Minimum-time reachability in timed games. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, volume 4596 of Lecture Notes in Computer Science, pages 825-837. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_71.
  6. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 66-80. Springer, 2005. URL: https://doi.org/10.1007/11539452_9.
  7. Franck Cassez, Thomas A. Henzinger, and Jean-François Raskin. A comparison of control problems for timed and hybrid systems. In Claire J. Tomlin and Mark R. Greenstreet, editors, Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002, Stanford, CA, USA, March 25-27, 2002, Proceedings, volume 2289 of Lecture Notes in Computer Science, pages 134-148. Springer, 2002. URL: https://doi.org/10.1007/3-540-45873-5_13.
  8. Franck Cassez, Jan Jakob Jessen, Kim Guldstrand Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic synthesis of robust and optimal controllers - an industrial case study. In Rupak Majumdar and Paulo Tabuada, editors, Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings, volume 5469 of Lecture Notes in Computer Science, pages 90-104. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00602-9_7.
  9. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In Roberto M. Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, volume 2761 of Lecture Notes in Computer Science, pages 142-156. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_9.
  10. Barbara Di Giampaolo, Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. Safraless procedures for timed specifications. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings, volume 6246 of Lecture Notes in Computer Science, pages 2-22. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15297-9_2.
  11. Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of real-time logics. In Joël Ouaknine and Frits W. Vaandrager, editors, Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 133-148. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04368-0_12.
  12. Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Efficient verification of real-time systems: compact data structure and state-space reduction. In Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), December 3-5, 1997, San Francisco, CA, USA, pages 14-24. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/REAL.1997.641265.
  13. Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP semantics: from timed models to timed implementations. Formal Aspects Comput., 17(3):319-341, 2005. URL: https://doi.org/10.1007/S00165-005-0067-8.
  14. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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