Regular set of representatives for time-constrained MSC graphs

详细信息	查看全文 | 推荐本文 |

• 作者：S. Akshay^a ; ^{akshay@irisa.fr} ; Blaise Genest^a ; ^b ; ^{blaise.genest@irisa.fr} ; Loï ; c Hé ; louë ; t^a ; ^{loic.helouet@irisa.fr} ; Shaofa Yang^c ; ^{sf.yang@siat.ac.cn}
• 关键词：Formal languages ; Formal methods ; Specification languages ; Timed automata ; Partial order languages ; MSC graphs ; Set of representatives
• 刊名：Information Processing Letters
• 出版年：2012
• 期刊代码：61_00200190
• 类别：cp
• 出版时间：15 August, 2012
• 卷：112
• 期：14-15
• 页码：592-598
• 文件大小：231 K

摘要

Systems involving both time and concurrency are notoriously difficult to analyze. Existing decidability results apply when clocks on different processes cannot be compared or when the set of timed executions is regular. We prove new decidability results for timed concurrent systems, requiring neither restriction. We consider the formalism of time-constrained MSC graphs (TC-MSC graphs for short) introduced in Akshay et al. (2007) , and study if the set of timed executions generated by a TC-MSC graph is empty. This emptiness problem is known to be undecidable in general (Gastin et al., 2009) . Our approach consists of finding a regular set R of representative timed executions, i.e., such that every timed execution of the system has an equivalent, up to commutation, timed execution in R. This allows us to solve the emptiness problem under the assumption that the TC-MSC graph is prohibited from (1) forcing any basic scenario to take an arbitrarily long time to complete and (2) enforcing unboundedly many events to occur within one unit of time.