Symbolically Bounding the Drift in Time-Constrained Message-Sequence-Chart Graphs

Title:Symbolically Bounding the Drift in Time-Constrained Message-Sequence-Chart Graphs
Speaker:Blaise Genest (CNRS researcher at IPAL, Singapore-France joint laboratory)
Time: 2:30pm, December 1st (Thursday), 2011
Venue:Lecture Room, Level 3, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract: Systems involving both time and concurrency are notoriously difficult to analyze. Existing decidability results apply in settings where clocks on different processes cannot be compared or where 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 (TCMSGs for short). We study the problem of checking whether the set of timed executions generated by a TCMSG is empty, which is undecidable in general.

In this paper, we show the decidability of this problem under the restriction that every path of the TCMSG is prohibited from forcing any basic scenario labeling a node to take more than K units of time to complete, for a given K. Further, we prove that this condition can be effectively checked. Our approach consists of encoding the time constraints seen along a path into a bounded system of inequalities. Instead of constructing an interleaved model and using zones of timed automata as in existing approaches, we symbolically manipulate the system of inequalities using the Fourier-Motzkin elimination method. This allows for decision procedures which are both efficient and handle non regular specifications.

Joint work with
S. Akshay, NUS, Singapore.
Loic Helouet, INRIA, Rennes, France.
Shaofa Yang, Chinese Academy of Science, SIAT, Shenzhen, China.

Bibliography:
Blaise Genest is a CNRS researcher at IPAL, a joint Laboratory between France and Singapore. His research interests include automata theory, concurrency theory, game theory, verification, bioinformatics and complex systems.

He obtained the doctor degree from LIAFA, University Paris 7, in 2004. Then he did one-year postdoc at University Warwick, UK. After that, he became a CNRS researcher at IRISA, University Rennes 1, France. From 2010 until now, he became a member of IPAL, the joint laboratory between France and Singapore.