Document Open Access Logo

Why Liveness for Timed Automata Is Hard, and What We Can Do About It

Authors Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.48.pdf
  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Author Details

Frédéric Herbreteau
B. Srivathsan
Thanh-Tung Tran
Igor Walukiewicz

Cite AsGet BibTex

Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why Liveness for Timed Automata Is Hard, and What We Can Do About It. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.48

Abstract

The liveness problem for timed automata asks if a given automaton has a run passing infinitely often through an accepting state. We show that unless P=NP, the liveness problem is more difficult than the reachability problem; more precisely, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is NP-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with the existing solutions.
Keywords
  • Timed automata
  • model-checking
  • liveness invariant
  • state subsumption

Metrics

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

References

  1. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  2. G. Behrmann, P. Bouyer, E. Fleury, and K. G. Larsen. Static guard analysis in timed automata verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 254-270. Springer, 2003. Google Scholar
  3. G. Behrmann, P. Bouyer, K. G. Larsen, and R. Pelánek. Lower and upper bounds in zone-based abstractions of timed automata. STTT, 8(3):204-215, 2006. Google Scholar
  4. C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In TACAS, volume 1384 of LNCS, pages 313-329, 1998. Google Scholar
  5. D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, pages 197-212, 1989. Google Scholar
  6. F. Herbreteau and B. Srivathsan. Coarse abstractions make zeno behaviours difficult to detect. Logical Methods in Computer Science, 9, 2013. Google Scholar
  7. F. Herbreteau, B. Srivathsan, and I. Walukiewicz. Better abstractions for timed automata. In LICS, pages 375-384. IEEE Computer Society, 2012. Google Scholar
  8. F. Herbreteau, B. Srivathsan, and I. Walukiewicz. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design, 40(2):122-146, 2012. Google Scholar
  9. F. Herbreteau, B. Srivathsan, and I. Walukiewicz. Lazy abstractions for timed automata. In CAV, volume 8044 of LNCS, pages 990-1005, 2013. Google Scholar
  10. F. Herbreteau and T.-T. Tran. Improving search order for reachability testing in timed automata. In FORMATS, pages 124-139. Springer, 2015. Google Scholar
  11. A. Laarman, M. C. Olesen, A. E. Dalsgaard, K. G. Larsen, and J. van de Pol. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In CAV, volume 8044 of LNCS, pages 968-983, 2013. Google Scholar
  12. G. Li. Checking timed Büchi automata emptiness using LU-abstractions. In FORMATS, pages 228-242, 2009. Google Scholar
  13. S. Tripakis. Checking timed büchi automata emptiness on simulation graphs. ACM Transactions on Computational Logic (TOCL), 10(3):15, 2009. Google Scholar
  14. S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001. Google Scholar
  15. S. Tripakis, S. Yovine, and A. Bouajjani. Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design, 26(3):267-292, 2005. Google Scholar
  16. UPPAAL. URL: http://www.uppaal.org.
  17. UPPAAL CSMA/CD model. http://www.it.uu.se/research/group/darts/uppaal/benchmarks/genCSMA_CD.awk. Accessed: 2014-10-08.
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