Abstract | ||
---|---|---|
Verifying systems involving both time and concurrency rapidly leads to undecidability, and requires restrictions to become effective. This paper addresses the emptiness problem for time-constrained MSC-Graphs (TC-MSC graphs for short), that is, checking whether there is a timed execution compatible with a TC-MSC graph specification. This problem is known to be undecidable in general [11], and decidable for some regular specifications [11]. We establish decidability of the emptiness problem under the condition that, for a given K, no path of the TC-MSC graph forces any node to take more than K time units to complete. We prove that this condition can be effectively checked. The proofs use a novel symbolic representation for runs, where time constraints are encoded as a system of inequalities. This allows us to handle non-regular specifications and improve efficiency w.r.t. using interleaved representations. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-32943-2_1 | ICTAC |
Keywords | Field | DocType |
novel symbolic representation,tc-msc graph,verifying system,emptiness problem,time-constrained msc graph,interleaved representation,non-regular specification,k time unit,efficiency w,time constraint,tc-msc graph specification | Discrete mathematics,Graph,Computer science,Concurrency,Theoretical computer science,Decidability,Mathematical proof,Emptiness,Unit of time,Undecidable problem,Bounding overwatch | Conference |
Citations | PageRank | References |
2 | 0.37 | 17 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
S. Akshay | 1 | 61 | 12.47 |
Blaise Genest | 2 | 304 | 25.09 |
Loïc Hélouët | 3 | 281 | 25.37 |
Shaofa Yang | 4 | 46 | 4.76 |