Document Open Access Logo

Simulations for Event-Clock Automata

Authors S. Akshay , Paul Gastin , R. Govind , B. Srivathsan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.13.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

S. Akshay
  • Department of CSE, Indian Institute of Technology Bombay, Mumbai, India
Paul Gastin
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
  • CNRS, ReLaX, IRL 2000, Siruseri, India
R. Govind
  • Department of CSE, Indian Institute of Technology Bombay, Mumbai, India
B. Srivathsan
  • Chennai Mathematical Institute, India
  • CNRS, ReLaX, IRL 2000, Siruseri, India

Funding

This work was supported by DST/CEFIPRA/INRIA Project EQuaVE.
  • Akshay, S.: Supported in part by DST/SERB Matrics Grant MTR/2018/000744.
  • Gastin, Paul: Partially supported by ANR project Ticktac (ANR-18-CE40-0015).

Cite As Get BibTex

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.13

Abstract

Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations.
In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Quantitative automata
  • Theory of computation → Logic and verification
Keywords
  • Event-clock automata
  • verification
  • zones
  • simulations
  • reachability

Metrics

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

Related Versions

References

  1. S. Akshay, Benedikt Bollig, and Paul Gastin. Event clock message passing automata: a logical characterization and an emptiness checking algorithm. Formal Methods Syst. Des., 42(3):262-300, 2013. Google Scholar
  2. S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for event-clock automata. CoRR, abs/2207.02633, 2022. Google Scholar
  3. S. Akshay, Paul Gastin, and Karthik R. Prakash. Fast zone-based algorithms for reachability in pushdown timed automata. In CAV (1), volume 12759 of Lecture Notes in Computer Science, pages 619-642. Springer, 2021. Google Scholar
  4. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994. Google Scholar
  5. Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci., 211(1-2):253-273, 1999. Google Scholar
  6. 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
  7. 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
  8. Patricia Bouyer. Forward analysis of updatable timed automata. Formal Methods Syst. Des., 24(3):281-320, 2004. Google Scholar
  9. Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic optimal reachability in weighted timed automata. In CAV (1), volume 9779 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. Google Scholar
  10. Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: A model-checking tool for real-time systems. In CAV, volume 1427 of Lecture Notes in Computer Science, pages 546-550. Springer, 1998. Google Scholar
  11. Laura Bozzelli, Angelo Montanari, and Adriano Peron. Taming the complexity of timeline-based planning over dense temporal domains. In FSTTCS, volume 150 of LIPIcs, pages 34:1-34:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  12. Laura Bozzelli, Angelo Montanari, and Adriano Peron. Complexity issues for timeline-based planning over dense time under future and minimal semantics. Theor. Comput. Sci., 901:87-113, 2022. Google Scholar
  13. 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
  14. David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197-212. Springer, 1989. Google Scholar
  15. Deepak D'Souza and Nicolas Tabareau. On timed automata with input-determined guards. In FORMATS/FTRTFT, volume 3253 of Lecture Notes in Computer Science, pages 68-83. Springer, 2004. Google Scholar
  16. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in timed automata with diagonal constraints. In CONCUR, volume 118 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  17. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 41-59. Springer, 2019. Google Scholar
  18. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability for updatable timed automata made faster and more effective. In FSTTCS, volume 182 of LIPIcs, pages 47:1-47:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  19. Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. Event clock automata: From theory to practice. In FORMATS, volume 6919 of Lecture Notes in Computer Science, pages 209-224. Springer, 2011. Google Scholar
  20. Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. On regions and zones for event-clock automata. Formal Methods Syst. Des., 45(3):330-380, 2014. Google Scholar
  21. Frédéric Herbreteau and Gerald Point. TChecker. https://github.com/fredher/tchecker, v0.2 - April 2019.
  22. 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
  23. 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
  24. Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, and Tom van Dijk. LTSmin: High-performance language-independent model checking. In TACAS, volume 9035 of Lecture Notes in Computer Science, pages 692-707. Springer, 2015. Google Scholar
  25. Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, and Andreas Podelski. Faster than UPPAAL? In CAV, volume 5123 of Lecture Notes in Computer Science, pages 552-555. Springer, 2008. Google Scholar
  26. Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. STTT, 1(1-2):134-152, 1997. Google Scholar
  27. Jean-François Raskin and Pierre-Yves Schobbens. The logic of event clocks - decidability, complexity and expressiveness. J. Autom. Lang. Comb., 4(3):247-282, 1999. Google Scholar
  28. Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction refinement algorithms for timed automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 22-40. Springer, 2019. Google Scholar
  29. Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. PAT: towards flexible verification under fairness. In CAV, volume 5643 of Lecture Notes in Computer Science, pages 709-714. Springer, 2009. Google Scholar
  30. Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, and István Majzik. Theta: A framework for abstraction refinement-based model checking. In FMCAD, pages 176-179. IEEE, 2017. Google Scholar
  31. Farn Wang. REDLIB for the formal verification of embedded systems. In ISoLA, pages 341-346. IEEE Computer Society, 2006. Google Scholar
  32. Jianhua Zhao, Xuandong Li, and Guoliang Zheng. A quadratic-time DBM-based successor algorithm for checking timed automata. Inf. Process. Lett., 96(3):101-105, 2005. 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