Document Open Access Logo

Reachability in Timed Automata with Diagonal Constraints

Authors Paul Gastin, Sayan Mukherjee, B. Srivathsan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.28.pdf
  • Filesize: 0.53 MB
  • 17 pages

Document Identifiers

Author Details

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

Funding

Partly supported by UMI RELAX, Infosys foundation (India) and Tata Consultancy Services - Innovation Labs (Pune, India)

Cite AsGet BibTex

Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in Timed Automata with Diagonal Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.28

Abstract

We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Timed Automata
  • Reachability
  • Zones
  • Diagonal constraints

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. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2004. Google Scholar
  4. Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, 36(2,3):145-182, 1998. Google Scholar
  5. Patricia Bouyer. Forward analysis of updatable timed automata. Formal Methods in System Design, 24(3):281-320, 2004. Google Scholar
  6. 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
  7. Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic optimal reachability in weighted timed automata. In Computer Aided Verification (CAV), volume 9779 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. Google Scholar
  8. Patricia Bouyer, François Laroussinie, and Pierre-Alain Reynier. Diagonal constraints in timed automata: Forward analysis of timed systems. In Formal Modeling and Analysis of Timed Systems (FORMATS), volume 3829 of Lecture Notes in Computer Science, pages 112-126. Springer, 2005. 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. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. Google Scholar
  11. 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
  12. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in timed automata with diagonal constraints. CoRR, abs/1806.11007, 2018. URL: http://arxiv.org/abs/1806.11007.
  13. Frédéric Herbreteau. TChecker. URL: http://www.labri.fr/perso/herbrete/tchecker/index.html.
  14. Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 13 of LIPIcs, pages 78-89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  15. 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
  16. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. Information and Computation, 251:67-90, 2016. Google Scholar
  17. Narendra Karmarkar. A new polynomial-time algorithm for linear programming. Combinatorica, 4(4):373-395, 1984. Google Scholar
  18. Pierre-Alain Reynier. Diagonal constraints handled efficiently in uppaal. In Research report LSV-07-02, Laboratoire Spécification et Vérification. ENS Cachan, France, 2007. Google Scholar
  19. 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
  20. Jianhua Zhao, Xuandong Li, and Guoliang Zheng. A quadratic-time dbm-based successor algorithm for checking timed automata. Information Processing Letters, 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 Imprint Privacy Contact