Document Open Access Logo

Analyzing Timed Systems Using Tree Automata

Authors S. Akshay, Paul Gastin, Shankara Narayanan Krishna

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.27.pdf
  • Filesize: 0.89 MB
  • 14 pages

Document Identifiers

Author Details

S. Akshay
Paul Gastin
Shankara Narayanan Krishna

Cite As Get BibTex

S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.27

Abstract

Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).

Subject Classification

Keywords
  • Timed automata
  • tree automata
  • pushdown systems
  • tree-width

Metrics

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

References

  1. P. Abdulla, M. F. Atig, and J. Stenman. Dense-timed pushdown automata. In LICS Proceedings, pages 35-44, 2012. Google Scholar
  2. C. Aiswarya and P. Gastin. Reasoning about distributed systems: WYSIWYG (invited talk). In FSTTCS Proceedings, pages 11-30, 2014. Google Scholar
  3. S. Akshay, P. Gastin, and S. N. Krishna. Analyzing timed systems using tree automata. CoRR, abs/1604.08443, 2016. URL: http://arxiv.org/abs/1604.08443.
  4. R. Alur and D. Dill. A theory of timed automata. In TCS, 126(2):183-235, 1994. Google Scholar
  5. M. F. Atig. Model-checking of ordered multi-pushdown automata. LMCS, 8(3), 2012. Google Scholar
  6. L. Clemente and S. Lasota. Timed pushdown automata revisited. In LICS Proceedings, pages 738-749, 2015. Google Scholar
  7. T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson. Introduction to Algorithms. McGraw-Hill Higher Education, 2nd edition, 2001. Google Scholar
  8. B. Courcelle. Special tree-width and the verification of monadic second-order graph properties. In FSTTCS Proceedings, pages 13-29, 2010. Google Scholar
  9. 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
  10. A. Cyriac. Verification of Communicating Recursive Programs via Split-width. Thèse de doctorat, LSV, ENS Cachan, January 2014. 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. W. Czerwinski, P. Hofman, and S. Lasota. Reachability problem for weak multi-pushdown automata. In CONCUR Proceedings, pages 53-68. Springer, 2012. Google Scholar
  13. S. N. Krishna, L. Manasa, and A. Trivedi. What’s decidable about recursive hybrid automata? In HSCC Proceedings, pages 31-40, 2015. Google Scholar
  14. S. La Torre, P. Madhusudan, and G. Parlato. The language theory of bounded context-switching. In LATIN Proceedings, pages 96-107, 2010. Google Scholar
  15. S. La Torre, M. Napoli, and G. Parlato. Scope-bounded pushdown languages. In DLT Proceedings, pages 116-128. Springer, 2014. Google Scholar
  16. S. La Torre, M. Napoli, and G. Parlato. A unifying approach for multistack pushdown automata. In MFCS Proceeedings, pages 377-389. Springer, 2014. Google Scholar
  17. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL Proceedings, pages 283-294, 2011. 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 About DROPS Imprint Privacy Contact