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. © 2012 Springer-Verlag.
CITATION STYLE
Akshay, S., Genest, B., Hélouët, L., & Yang, S. (2012). Symbolically bounding the drift in time-constrained MSC graphs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7521 LNCS, pp. 1–15). https://doi.org/10.1007/978-3-642-32943-2_1
Mendeley helps you to discover research relevant for your work.