Towards an Efficient Tree Automata Based Technique for Timed Systems

Authors S. Akshay, Paul Gastin, Shankara Narayanan Krishna, Ilias Sarkar



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.39.pdf
  • Filesize: 0.92 MB
  • 15 pages

Document Identifiers

Author Details

S. Akshay
Paul Gastin
Shankara Narayanan Krishna
Ilias Sarkar

Cite AsGet BibTex

S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarkar. Towards an Efficient Tree Automata Based Technique for Timed Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.39

Abstract

The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.
Keywords
  • Timed automata
  • tree automata
  • pushdown systems
  • tree-width

Metrics

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

References

  1. P. Abdulla, M. F. Atig, and J. Stenman. Dense-timed pushdown automata. In LICS Proceedings, pages 35-44, 2012. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. The minimal cost reachability problem in priced timed pushdown systems. In Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings, pages 58-69, 2012. Google Scholar
  3. C. Aiswarya and P. Gastin. Reasoning about distributed systems: WYSIWYG (invited talk). In FSTTCS Proceedings, pages 11-30, 2014. Google Scholar
  4. S. Akshay, P. Gastin, and S. Krishna. Analyzing timed systems using tree automata. In CONCUR Proceedings, 2016. Google Scholar
  5. S. Akshay, P. Gastin, S. N. Krishna, and I. Sarkar. Towards an efficient tree automata based technique for timed systems. CoRR, abs/1707.02297, 2017. URL: http://arxiv.org/abs/1707.02297.
  6. R. Alur and D. Dill. A theory of timed automata. In TCS, 126(2):183-235, 1994. Google Scholar
  7. G. Behrmann, A. David, and K. G. Larsen. A tutorial on Uppaal. In International School on Formal Methods for the Design of Computer, Communication and Software Systems, pages 200-236, 2004. Google Scholar
  8. A. Bouajjani, R. Echahed, and R. Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, pages 64-85, 1994. Google Scholar
  9. L. Clemente and S. Lasota. Timed pushdown automata revisited. In LICS Proceedings, pages 738-749, 2015. Google Scholar
  10. B. Courcelle and J. Engelfriet. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications. CUP, 2012. Google Scholar
  11. A. Cyriac, P. Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR Proceedings, pages 547-561, 2012. Google Scholar
  12. Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, and Shoji Yuen. Nested timed automata. In Formal Modeling and Analysis of Timed Systems - 11th International Conference, FORMATS 2013, Buenos Aires, Argentina, August 29-31, 2013. Proceedings, pages 168-182, 2013. Google Scholar
  13. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL Proceedings, pages 283-294, 2011. Google Scholar
  14. Ashutosh Trivedi and Dominik Wojtczak. Recursive timed automata. In ATVA Proceedings, pages 306-324, 2010. 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