Document Open Access Logo

Parametric Disjunctive Timed Networks

Authors Étienne André , Swen Jacobs , Engel Lefaucheux

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.31.pdf
  • Filesize: 1.15 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Model checking
Keywords
  • parametrised verification
  • parametric timed automata
  • verification of infinite-state systems

Metrics

Abstract

We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.

Cite As Get BibTex

Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.31

Author Details

Étienne André
  • Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030, Villetaneuse, France
  • Institut universitaire de France (IUF), Paris, France
  • Nantes Université, CNRS, LS2N, Nantes, Bretagne, France
Swen Jacobs
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Engel Lefaucheux
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Funding

This work is partially supported by ANR BisoUS (ANR-22-CE48-0012).
  • André, Étienne: Partially supported by ANR TAPAS (ANR-24-CE25-5742).
  • Lefaucheux, Engel: Partially supported by ANR GUMMIS (ANR-25-CE48-5096).

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Timed lossy channel systems. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, FSTTCS, volume 18 of LIPIcs, pages 374-386. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.374.
  2. Parosh Aziz Abdulla and Giorgio Delzanno. Parameterized verification. International Journal on Software Tools for Technology Transfer, 18(5):469-473, 2016. URL: https://doi.org/10.1007/s10009-016-0424-3.
  3. Parosh Aziz Abdulla, Giorgio Delzanno, Othmane Rezine, Arnaud Sangnier, and Riccardo Traverso. Parameterized verification of time-sensitive models of ad hoc network protocols. Theoretical Computer Science, 612:1-22, 2016. URL: https://doi.org/10.1016/j.tcs.2015.07.048.
  4. Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In LiCS, pages 345-354. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319629.
  5. Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241-264, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00330-9.
  6. Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Edmund M Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 685-725. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_21.
  7. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, April 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  8. Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC, pages 592-601, New York, NY, USA, 1993. ACM. URL: https://doi.org/10.1145/167088.167242.
  9. Étienne André. What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer, 21(2):203-219, April 2019. URL: https://doi.org/10.1007/s10009-017-0467-0.
  10. Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-time opacity problems in one-clock parametric timed automata. In Siddharth Barman and Sławomir Lasota, editors, FSTTCS, volume 323 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, December 2024. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.3.
  11. Étienne André, Benoît Delahaye, Paulin Fournier, and Didier Lime. Parametric timed broadcast protocols. In Constantin Enea and Ruzica Piskac, editors, VMCAI, volume 11388 of Lecture Notes in Computer Science, pages 491-512. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-11245-5_23.
  12. Étienne André, Paul Eichler, Swen Jacobs, and Shyam Lal Karra. Parameterized verification of disjunctive timed networks. In Rayna Dimitrova and Ori Lahav, editors, VMCAI, volume 14499 of Lecture Notes in Computer Science, pages 124-146. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-50524-9_6.
  13. Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur. Parameterized verification of timed networks with clock invariants. In C Aiswarya, Ruta Mehta, and Subhajit Roy, editors, FSTTCS, December 2025. To appear. Google Scholar
  14. Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric disjunctive timed networks (full version). Technical report, arXiv, 2025. URL: https://doi.org/10.48550/arXiv.2512.04991.
  15. Étienne André, Michał Knapik, Wojciech Penczek, and Laure Petrucci. Controlling actions and time in parametric timed automata. In Jörg Desel and Alex Yakovlev, editors, ACSD, pages 45-54. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/ACSD.2016.20.
  16. Étienne André, Didier Lime, and Nicolas Markey. Language preservation problems in parametric timed automata. Logical Methods in Computer Science, 16(1), January 2020. URL: https://doi.org/10.23638/LMCS-16(1:5)2020.
  17. Étienne André, Didier Lime, and Olivier H. Roux. Reachability and liveness in parametric timed automata. Logical Methods in Computer Science, 18(1):31:1-31:41, February 2022. URL: https://doi.org/10.46298/lmcs-18(1:31)2022.
  18. Nikola Beneš, Peter Bezděk, Kim Guldstrand Larsen, and Jiří Srba. Language emptiness of continuous-time parametric timed automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP, Part II, volume 9135 of Lecture Notes in Computer Science, pages 69-81. Springer, July 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_6.
  19. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
  20. Olaf Burkart and Bernhard Steffen. Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89-125, 1995. Google Scholar
  21. Giorgio Delzanno and Pierre Ganty. Automatic verification of time sensitive cryptographic protocols. In Kurt Jensen and Andreas Podelski, editors, TACAS, volume 2988 of Lecture Notes in Computer Science, pages 342-356. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_27.
  22. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Paul Gastin and François Laroussinie, editors, CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 313-327. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_22.
  23. Javier Esparza, Mikhail A. Raskin, and Chana Weil-Kennedy. Parameterized analysis of immediate observation Petri nets. In Susanna Donatelli and Stefan Haar, editors, Petri Nets, volume 11522 of Lecture Notes in Computer Science, pages 365-385. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-21571-2_20.
  24. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems, 34(1):6:1-6:48, 2012. URL: https://doi.org/10.1145/2160910.2160915.
  25. Carlo Ghezzi, Dino Mandrioli, Sandro Morasca, and Mauro Pezzè. A unified high-level Petri net formalism for time-critical systems. IEEE Transactions on Software Engineering, 17(2):160-172, 1991. URL: https://doi.org/10.1109/32.67597.
  26. Stefan Göller and Mathieu Hilaire. Reachability in two-parametric timed automata with one parameter is expspace-complete. Theoretical Computer Science, 68(4):900-985, 2024. URL: https://doi.org/10.1007/S00224-023-10121-3.
  27. Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 52-53:183-220, 2002. URL: https://doi.org/10.1016/S1567-8326(02)00037-1.
  28. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In LiCS, pages 667-676. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.67.
  29. Engel Lefaucheux. When are two parametric semi-linear sets equal? Technical Report hal-04172593, HAL, 2024. URL: https://inria.hal.science/hal-04172593.
  30. Li Li, Jun Sun, Yang Liu, and Jin Song Dong. Verifying parameterized timed security protocols. In Nikolaj Bjørner and Frank S. de Boer, editors, FM, volume 9109 of Lecture Notes in Computer Science, pages 342-359. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19249-9_22.
  31. Philip Meir Merlin and David J. Farber. Recoverability of communication protocols-implications of a theoretical study. IEEE Transactions on Communications, 24(9):1036-1043, 1976. URL: https://doi.org/10.1109/TCOM.1976.1093424.
  32. Marvin L. Minsky. Computation: Finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967. Google Scholar
  33. Chander Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Technology, USA, 1973. URL: http://hdl.handle.net/1721.1/13739.
  34. Mikhail A. Raskin, Chana Weil-Kennedy, and Javier Esparza. Flatness and complexity of immediate observation Petri nets. In Igor Konnov and Laura Kovács, editors, CONCUR, volume 171 of LIPIcs, pages 45:1-45:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.45.
  35. Luca Spalazzi and Francesco Spegni. Parameterized model checking of networks of timed automata with Boolean guards. Theoretical Computer Science, 813:248-269, 2020. URL: https://doi.org/10.1016/j.tcs.2019.12.026.
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