文章基本信息

标题：Verification of Timed Asynchronous Programs
本地全文：下载
作者：Parosh Aziz Abdulla ; Mohamed Faouzi Atig ; Shankara Narayanan Krishna 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-16
DOI：10.4230/LIPIcs.FSTTCS.2018.8
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Reachability; Timed Automata; Asynchronous programs