Search Results

Documents authored by Sarkar, Ilias


Document
Towards an Efficient Tree Automata Based Technique for Timed Systems

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

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.39,
  author =	{Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
  title =	{{Towards an Efficient Tree Automata Based Technique for Timed Systems}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{39:1--39:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.39},
  URN =		{urn:nbn:de:0030-drops-78017},
  doi =		{10.4230/LIPIcs.CONCUR.2017.39},
  annote =	{Keywords: Timed automata, tree automata, pushdown systems, tree-width}
}
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