Document Open Access Logo

Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics

Authors Frédéric Herbreteau , B. Srivathsan , Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.12.pdf
  • Filesize: 0.84 MB
  • 24 pages

Document Identifiers

Author Details

Frédéric Herbreteau
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
B. Srivathsan
  • Chennai Mathematical Institute, India
  • CNRS IRL 2000, ReLaX, Chennai, India
Igor Walukiewicz
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France

Funding

  • Herbreteau, Frédéric: ANR project Ticktak (ANR-18-CE40-0015)
  • Walukiewicz, Igor: ANR project Ticktac (ANR-18-CE40-0015)

Cite AsGet BibTex

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.12

Abstract

We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline. Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency. In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Timed Büchi automata
  • local-time semantics
  • zones
  • abstraction
  • partial-order reduction

Metrics

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

References

  1. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Source sets: A foundation for optimal dynamic partial order reduction. J. ACM, 64(4):25:1-25:49, 2017. URL: https://doi.org/10.1145/3073408.
  2. 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.
  3. Étienne André, Jaime Arias, Laure Petrucci, and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 311-329. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_17.
  4. Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf., 8(3):204-215, 2006. Google Scholar
  5. Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. Partial order reductions for timed systems. In CONCUR, volume 1466 of Lecture Notes in Computer Science, pages 485-500, 1998. Google Scholar
  6. Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz, and Jirí Srba. Stubborn set reduction for two-player reachability games. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7278.
  7. Patricia Bouyer. Forward analysis of updatable timed automata. Formal Methods Syst. Des., 24(3):281-320, 2004. Google Scholar
  8. Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier, and Ocan Sankur. Robust controller synthesis in timed büchi automata: A symbolic approach. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 572-590. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_33.
  9. Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. Value-centric dynamic partial order reduction. Proc. ACM Program. Lang., 3(OOPSLA):124:1-124:29, 2019. URL: https://doi.org/10.1145/3360550.
  10. Dennis Dams, Rob Gerth, Bart Knaack, and Ruurd Kuiper. Partial-order reduction techniques for real-time model checking. Formal Aspects Comput., 10(5-6):469-482, 1998. URL: https://doi.org/10.1007/s001650050028.
  11. Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. In TACAS, volume 1384 of Lecture Notes in Computer Science, pages 313-329. Springer, 1998. Google Scholar
  12. Laurent Fribourg. A closed-form evaluation for extended timed automata. Technical report, CNRS and École Normale Supérieure de Cachan, 1998. Google Scholar
  13. Patrice Godefroid and Pierre Wolper. A partial approach to model checking. Inf. Comput., 110(2):305-326, 1994. URL: https://doi.org/10.1006/inco.1994.1035.
  14. R. Govind. Partial-order reduction for timed systems. PhD thesis, Université de Bordeaux, France and Chennai Mathematical Institute, India (cotutelle), 2021. Google Scholar
  15. R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Abstractions for the Local-time Semantics of Timed Automata: a Foundation for Partial-order Methods. To appear at 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. URL: https://hal.archives-ouvertes.fr/hal-03644039.
  16. R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting local time semantics for networks of timed automata. In CONCUR, volume 140 of LIPIcs, pages 16:1-16:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  17. Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, and Jun Sun. Diamonds are a girl’s best friend: Partial order reduction for timed automata with abstractions. In CAV, volume 8559 of Lecture Notes in Computer Science, pages 391-406. Springer, 2014. Google Scholar
  18. Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why liveness for timed automata is hard, and what we can do about it. ACM Trans. Comput. Log., 21(3):17:1-17:28, 2020. Google Scholar
  19. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient emptiness check for timed büchi automata. Formal Methods Syst. Des., 40(2):122-146, 2012. Google Scholar
  20. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Lazy abstractions for timed automata. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 990-1005. Springer, 2013. Google Scholar
  21. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. Inf. Comput., 251:67-90, 2016. URL: https://doi.org/10.1016/j.ic.2016.07.004.
  22. Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498711.
  23. Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, and Jaco van de Pol. Multi-core emptiness checking of timed büchi automata using inclusion abstraction. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 968-983. Springer, 2013. Google Scholar
  24. Kim G. Larsen, Marius Mikucionis, Marco Muñiz, and Jirí Srba. Urgent partial order reduction for extended timed automata. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 179-195. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_10.
  25. Guangyuan Li. Checking timed büchi automata emptiness using lu-abstractions. In FORMATS, volume 5813 of Lecture Notes in Computer Science, pages 228-242. Springer, 2009. Google Scholar
  26. Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. Electron. Notes Theor. Comput. Sci., 23(2):88-107, 1999. URL: https://doi.org/10.1016/S1571-0661(04)80671-6.
  27. Doron A. Peled. All from one, one for all: on model checking using representatives. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 409-423. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_34.
  28. Stavros Tripakis. Checking timed büchi automata emptiness on simulation graphs. ACM Trans. Comput. Log., 10(3):15:1-15:19, 2009. Google Scholar
  29. Stavros Tripakis, Sergio Yovine, and Ahmed Bouajjani. Checking timed Büchi automata emptiness efficiently. Form. Methods Syst. Des., 26(3):267-292, 2005. Google Scholar
  30. Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science, pages 491-515. Springer, 1989. URL: https://doi.org/10.1007/3-540-53863-1_36.
  31. Antti Valmari. Stop it, and be stubborn! ACM Trans. Embed. Comput. Syst., 16(2):46:1-46:26, 2017. URL: https://doi.org/10.1145/3012279.
  32. Antti Valmari and Henri Hansen. Stubborn set intuition explained. Trans. Petri Nets Other Model. Concurr., 12:140-165, 2017. URL: https://doi.org/10.1007/978-3-662-55862-1_7.
  33. Naling Zhang, Markus Kusano, and Chao Wang. Dynamic partial order reduction for relaxed memory models. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 250-259. ACM, 2015. URL: https://doi.org/10.1145/2737924.2737956.
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