Document Open Access Logo

Verification of Timed Asynchronous Programs

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2018.8.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Reachability
  • Timed Automata
  • Asynchronous programs

Metrics

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

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.8

Author Details

Parosh Aziz Abdulla
  • Uppsala University, Sweden
Mohamed Faouzi Atig
  • Uppsala University, Sweden
Shankara Narayanan Krishna
  • IIT Bombay, India
Shaan Vaidya
  • IIT Bombay, India

References

  1. P.A. Abdulla, M. Faouzi Atig, S. Krishna, and S. Vaidya. Verification of Timed Asynchronous Programs. URL: http://www.cse.iitb.ac.in/~krishnas/fsttcs2018.pdf.
  2. Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci., 126(2):183-235, April 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90010-8.
  3. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verification of Asynchronous Programs with Nested Locks. In Satya V. Lokam and R. Ramanujam, editors, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, volume 93 of LIPIcs, pages 11:1-11:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2017.11.
  4. Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. Analyzing Asynchronous Programs with Preemption. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India, volume 2 of LIPIcs, pages 37-48. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2008.1739.
  5. Rohit Chadha and Mahesh Viswanathan. Decidability Results for Well-Structured Transition Systems with Auxiliary Storage. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 136-150. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74407-8_10.
  6. Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric. Delay-bounded scheduling. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 411-422. ACM, 2011. URL: http://dx.doi.org/10.1145/1926385.1926432.
  7. Pierre Ganty and Rupak Majumdar. Analyzing Real-Time Event-Driven Programs. In Joël Ouaknine and Frits W. Vaandrager, editors, Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 164-178. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04368-0_14.
  8. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, 2012. URL: http://dx.doi.org/10.1145/2160910.2160915.
  9. Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen. The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 355-364. IEEE Computer Society, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.46.
  10. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  11. Ranjit Jhala and Rupak Majumdar. Interprocedural analysis of asynchronous programs. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 339-350. ACM, 2007. URL: http://dx.doi.org/10.1145/1190216.1190266.
  12. Joseph B Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3):297-305, 1972. Google Scholar
  13. Pallavi Maiya, Rahul Gupta, Aditya Kanade, and Rupak Majumdar. Partial Order Reduction for Event-Driven Multi-threaded Programs. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS, volume 9636 of Lecture Notes in Computer Science, pages 680-697. Springer, 2016. Google Scholar
  14. Rupak Majumdar and Zilong Wang. Bbs: A Phase-Bounded Model Checker for Asynchronous Programs. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 496-503. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21690-4_33.
  15. M. Minsky. Computation: Finite and Infinite Machines. Prentice Hall International, 1967. Google Scholar
  16. Koushik Sen and Mahesh Viswanathan. Model Checking Multithreaded Programs with Asynchronous Atomic Methods. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 300-314. Springer, 2006. URL: http://dx.doi.org/10.1007/11817963_29.
  17. Jiří Srba. Timed-Arc Petri Nets vs. Networks of Timed Automata. In Proceedings of the 26th International Conference on Application and Theory of Petri Nets (ICATPN 2005). Netherlands: Springer-Verlag, 2005, pages 385-402, 2005. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact