Document Open Access Logo

Revisiting Local Time Semantics for Networks of Timed Automata

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.16.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

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

Funding

Work supported by UMI 2000 ReLaX, ANR project TickTac, and project IoTTTA - CEFIPRA Indo-French program in ICST - DST/CNRS ref. 2016-01. Author B. Srivathsan is partially funded by grants from Infosys Foundation, India and Tata Consultancy Services, India.

Cite As Get BibTex

R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting Local Time Semantics for Networks of Timed Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.16

Abstract

We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone.
We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Timed automata
  • verification
  • local-time semantics
  • abstraction

Metrics

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

Related Versions

References

  1. Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126:183-235, 1994. Google Scholar
  2. Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, and Radek Pelánek. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer, 8(3):204-215, 2006. Google Scholar
  3. Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Hakansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In QEST, pages 125-126. IEEE Computer Society, 2006. Google Scholar
  4. 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
  5. Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. In ACPN 2003, volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2003. Google Scholar
  6. Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz, and Jirí Srba. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In CAV, volume 10981 of Lecture Notes in Computer Science, pages 527-546. Springer, 2018. Google Scholar
  7. 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
  8. D. L. Dill. Timing Assumptions and Verification of Finite-state Concurrent Systems. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pages 197-212, 1990. Google Scholar
  9. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. CoRR, abs/1904.08590, 2019. URL: http://arxiv.org/abs/1904.08590.
  10. R Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting local time semantics for networks of timed automata. CoRR, abs/1907.02296, 2019. URL: http://arxiv.org/abs/1907.02296.
  11. F. Herbreteau and G. Point. TChecker. https://github.com/fredher/tchecker, v0.2 - April 2019.
  12. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better Abstractions for Timed Automata. In LICS, pages 375-384. IEEE Computer Society, 2012. Google Scholar
  13. Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. STTT, 1(1-2):134-152, 1997. Google Scholar
  14. Denis Lugiez, Peter Niebert, and Sarah Zennou. A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci., 345(1):27-59, 2005. Google Scholar
  15. Marius Minea. Partial Order Reduction for Model Checking of Timed Automata. In CONCUR, volume 1664 of Lecture Notes in Computer Science, pages 431-446. Springer, 1999. Google Scholar
  16. Marius Minea. Partial Order Reduction for Verification of Timed Systems. PhD thesis, School of Computer Science, Carnegie Mellon University Pittsburgh, PA 15213, 1999. Google Scholar
  17. Ramzi Ben Salah, Marius Bozga, and Oded Maler. On Interleaving in Timed Automata. In CONCUR, volume 4137 of Lecture Notes in Computer Science, pages 465-476. Springer, 2006. Google Scholar
  18. Marcelo Sousa, César Rodríguez, Vijay D'Silva, and Daniel Kroening. Abstract Interpretation with Unfoldings. In CAV, pages 197-216, 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 About DROPS Imprint Privacy Contact