Document Open Access Logo

Reachability for Updatable Timed Automata Made Faster and More Effective

Authors Paul Gastin , Sayan Mukherjee , B Srivathsan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.47.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Paul Gastin
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Sayan Mukherjee
  • Chennai Mathematical Institute, India
B Srivathsan
  • Chennai Mathematical Institute, India

Funding

Work supported by IRL ReLaX. Paul Gastin is supported by ANR project TickTac (ANR-18-CE40-0015). B Srivathsan is supported by CEFIPRA project IoTTTA (DST/CNRS ref. 2016-01). Sayan Mukherjee and B Srivathsan are additionally supported by Infosys Foundation (India).

Cite AsGet BibTex

Paul Gastin, Sayan Mukherjee, and B Srivathsan. Reachability for Updatable Timed Automata Made Faster and More Effective. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47

Abstract

Updatable timed automata (UTA) are extensions of classical timed automata that allow special updates to clock variables, like x: = x - 1, x : = y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Updatable timed automata
  • Reachability
  • Zones
  • Simulations
  • Static analysis

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(2):183-235, 1994. Google Scholar
  2. Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. TIMES: A tool for schedulability analysis and code generation of real-time systems. In Formal Modeling and Analysis of Timed Systems (FORMATS), volume 2791 of Lecture Notes in Computer Science, pages 60-72. Springer, 2003. Google Scholar
  3. Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, and Kim G. Larsen. Static guard analysis in timed automata verification. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 254-270. Springer, 2003. Google Scholar
  4. 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
  5. Mikolaj Bojanczyk and Slawomir Lasota. A machine-independent characterization of timed languages. In International Colloquium on Automata, Languages and Programming (ICALP), volume 7392 of Lecture Notes in Computer Science, pages 92-103. Springer, 2012. Google Scholar
  6. Patricia Bouyer. Forward analysis of updatable timed automata. Formal Methods in System Design, 24(3):281-320, 2004. Google Scholar
  7. Patricia Bouyer and Fabrice Chevalier. On conciseness of extensions of timed automata. Journal of Automata, Languages and Combinatorics, 10(4):393-405, 2005. Google Scholar
  8. Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Updatable timed automata. Theoretical Computer Science, 321(2-3):291-345, 2004. Google Scholar
  9. Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1384 of Lecture Notes in Computer Science, pages 313-329. Springer, 1998. Google Scholar
  10. 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
  11. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is pspace-complete. Inf. Comput., 243:26-36, 2015. Google Scholar
  12. Elena Fersman, Pavel Krcál, Paul Pettersson, and Wang Yi. Task automata: Schedulability, decidability and undecidability. Inf. Comput., 205(8):1149-1172, 2007. Google Scholar
  13. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in timed automata with diagonal constraints. In International Conference on Concurrency Theory (CONCUR), volume 118 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  14. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. In Computer Aided Verification (CAV), pages 41-59, Cham, 2019. Springer International Publishing. Google Scholar
  15. Paul Gastin, Sayan Mukherjee, and B Srivathsan. Reachability for updatable timed automata made faster and more effective, 2020. URL: http://arxiv.org/abs/2009.13260.
  16. Thorsten Gerdsmeier and Rachel Cardell-Oliver. Analysis of scheduling behaviour using generic timed automata. Electronic Notes in Theoretical Computer Science, 42:143-157, 2001. Computing: The Australasian Theory Symposium (CATS). Google Scholar
  17. Christoph Haase, Joël Ouaknine, and James Worrell. Relating reachability problems in timed and counter automata. Fundam. Inform., 143(3-4):317-338, 2016. Google Scholar
  18. Leo Hatvani, Alexandre David, Cristina Cerschi Seceleanu, and Paul Pettersson. Adaptive task automata with earliest-deadline-first scheduling. ECEASST, 70, 2014. Google Scholar
  19. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? J. Comput. Syst. Sci., 57(1):94-124, 1998. Google Scholar
  20. Frédéric Herbreteau and Gerald Point. TChecker. URL: https://github.com/ticktac-project/tchecker.
  21. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Lazy abstractions for timed automata. In Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 990-1005. Springer, 2013. Google Scholar
  22. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. Information and Computation, 251:67-90, 2016. Google Scholar
  23. Pavel Krcál, Martin Stigge, and Wang Yi. Multi-processor schedulability analysis of preemptive real-time tasks with variable execution times. In Formal Modeling and Analysis of Timed Systems (FORMATS), volume 4763 of Lecture Notes in Computer Science, pages 274-289. Springer, 2007. Google Scholar
  24. Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997. Google Scholar
  25. Yuki Osada, Tim French, Mark Reynolds, and Harry Smallbone. Hourglass automata. In Games, Automata, Logic and Formal verification (GandALF), volume 161 of EPTCS, pages 175-188, 2014. Google Scholar
  26. Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction refinement algorithms for timed automata. In Computer Aided Verification (CAV), volume 11561 of Lecture Notes in Computer Science, pages 22-40. Springer, 2019. Google Scholar
  27. Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. Pat: Towards flexible verification under fairness. In Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 709-714. Springer, 2009. Google Scholar
  28. 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 Daryl Stewart and Georg Weissenbacher, editors, Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 176-179, 2017. URL: https://doi.org/10.23919/FMCAD.2017.8102257.
  29. Sergio Yovine. Kronos: A verification tool for real-time systems. (Kronos user’s manual release 2.2). International Journal on Software Tools for Technology Transfer, 1:123-133, 1997. 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 Imprint Privacy Contact