Document Open Access Logo

A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets

Authors Kyveli Doveri , Pierre Ganty , B. Srivathsan

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2024.21.pdf
  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Timed languages
  • Timed automata
  • Canonical representation
  • Myhill-Nerode equivalence
  • Integer reset

Metrics

Abstract

The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages.
In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.

Cite As Get BibTex

Kyveli Doveri, Pierre Ganty, and B. Srivathsan. A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.21

Author Details

Kyveli Doveri
  • University of Warsaw, Poland
Pierre Ganty
  • IMDEA Software Institute, Pozuelo de Alarcón, Madrid, Spain
B. Srivathsan
  • Chennai Mathematical Institute, India
  • CNRS IRL 2000, ReLaX, Chennai, India

Funding

  • Doveri, Kyveli: Supported by the ERC grant INFSYS, agreement no. 950398. Results partly obtained when previously affiliated with the IMDEA Software Institute.
  • Ganty, Pierre: This publication is part of the grant PID2022-138072OB-I00, funded by MCIN/AEI/10.13039/501100011033/FEDER, UE.

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning one-clock timed automata. In TACAS'20: Proc. 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 12078 of LNCS, pages 444-462. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_25.
  3. Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning Nondeterministic Real-Time Automata. ACM Transactions on Embedded Computing Systems, 20(5s):1-26, 2021. URL: https://doi.org/10.1145/3477030.
  4. Dana Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87-106, 1987. URL: https://doi.org/10.1016/0890-5401(87)90052-6.
  5. Devendra Bhave and Shibashis Guha. Adding Dense-Timed Stack to Integer Reset Timed Automata. In RP'17: Proc. 11th International Conference on Reachability Problems, volume 10506 of LNCS, pages 9-25. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67089-8_2.
  6. Mikołaj Bojańczyk and Sławomir Lasota. A Machine-Independent Characterization of Timed Languages. In ICALP'12: Proc. of the 39th Int. Colloquium of Automata, Languages and Programming, volume 7392, pages 92-103. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31585-5_12.
  7. Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Updatable timed automata. Theoretical Computer Science, 321(2-3):291-345, 2004. URL: https://doi.org/10.1016/j.tcs.2004.04.003.
  8. Véronique Bruyère, Bharat Garhewal, Guillermo A. Pérez, Gaëtan Staquet, and Frits W. Vaandrager. Active learning of mealy machines with timers. CoRR, abs/2403.02019, 2024. URL: https://doi.org/10.48550/arxiv.2403.02019.
  9. Kyveli Doveri, Pierre Ganty, and B. Srivathsan. A myhill-nerode style characterization for timed automata with integer resets. CoRR, abs/2410.02464, 2024. URL: https://doi.org/10.48550/arxiv.2410.02464.
  10. Olga Grinchtein, Bengt Jonsson, and Martin Leucker. Learning of event-recording automata. Theoretical Computer Science, 411(47):4029-4054, 2010. URL: https://doi.org/10.1016/j.tcs.2010.07.008.
  11. Olga Grinchtein, Bengt Jonsson, and Paul Pettersson. Inference of event-recording automata using timed decision trees. In CONCUR'06: Proc. 17th International Conference on Concurrency Theory, volume 4137 of LNCS, pages 435-449. Springer, 2006. URL: https://doi.org/10.1007/11817949_29.
  12. Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, and Yang Liu. An efficient algorithm for learning event-recording automata. In ATVA'11: Proc. 9th International Symposium on Automated Technology for Verification and Analysis, volume 6996 of LNCS, pages 463-472. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24372-1_35.
  13. Anirban Majumdar, Sayan Mukherjee, and Jean-François Raskin. Greybox learning of languages recognizable by event-recording automata. In ATVA'24: Proc. 22nd International Symposium on Automated Technology for Verification and Analysis, LNCS. Springer, 2024. Google Scholar
  14. Oded Maler and Amir Pnueli. On Recognizable Timed Languages. In FoSSaCS'04: Proc. of the Int. Conf. on Foundations of Software Science and Computation Structures, volume 2987 of LNCS, pages 348-362. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_25.
  15. Lakshmi Manasa and Krishna S. Integer Reset Timed Automata: Clock Reduction and Determinizability. CoRR, abs/1001.1215, 2010. URL: https://doi.org/10.48550/arxiv.1001.1215.
  16. Jan Springintveld and Frits W. Vaandrager. Minimizable timed automata. In FTRTFT'96: Proc. of 4th Int. Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of LNCS, pages 130-147. Springer, 1996. URL: https://doi.org/10.1007/3-540-61648-9_38.
  17. P. Vijay Suman, Paritosh K. Pandya, Shankara Narayanan Krishna, and Lakshmi Manasa. Timed Automata with Integer Resets: Language Inclusion and Expressiveness. In FORMATS'08: Proc. of the Int. Conf. on Formal Modeling and Analysis of Timed Systems, volume 5215, pages 78-92. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_7.
  18. Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. Time to learn - learning timed automata from tests. In FORMATS'19: Proc. 17th International Conference on Formal Modeling and Analysis of Timed Systems, volume 11750 of LNCS, pages 216-235. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29662-9_13.
  19. Frits W. Vaandrager, Masoud Ebrahimi, and Roderick Bloem. Learning mealy machines with one timer. Inf. Comput., 295(Part B):105013, 2023. URL: https://doi.org/10.1016/J.IC.2023.105013.
  20. Sicco Verwer. Efficient Identification of Timed Automata: Theory and practice. PhD thesis, Delft University of Technology, Netherlands, 2010. URL: http://resolver.tudelft.nl/uuid:61d9f199-7b01-45be-a6ed-04498113a212.
  21. Masaki Waga. Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. In CAV'23: Proc. of the 35th Int. Conf. on Computer Aided Verification, volume 13964 of LNCS, pages 3-26. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37706-8_1.
  22. Runqing Xu, Jie An, and Bohua Zhan. Active learning of one-clock timed automata using constraint solving. In ATVA'22: Proc. 20th International Symposium on Automated Technology for Verification and Analysis, volume 13505 of LNCS, pages 249-265. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-19992-9_16.
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