DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2018.8

Verification of Timed Asynchronous Programs

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract

In this paper, we address the verification problem for timed asynchronous programs. We associate to each task, a deadline for its execution. We first show that the control state reachability problem for such class of systems is decidable while the configuration reachability problem is undecidable. Then, we consider the subclass of timed asynchronous programs where tasks are always being executed from the same state. For this subclass, we show that the control state reachability problem is PSPACE-complete. Furthermore, we show the decidability for the configuration reachability problem for the subclass.

Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya. Verification of Timed Asynchronous Programs. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2018.8,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Krishna, Shankara Narayanan and Vaidya, Shaan},
  title =	{{Verification of Timed Asynchronous Programs}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.8},
  URN =		{urn:nbn:de:0030-drops-99076},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.8},
  annote =	{Keywords: Reachability, Timed Automata, Asynchronous programs}
}

Search Results

Documents authored by Vaidya, Shaan

Verification of Timed Asynchronous Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message