Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis

The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithms of dense-time automata. The time progress operator takes the concavity of a path condition into consideration and usually results in high complexity in the evaluation. Previous algorithms in this aspect usually assume that the location invariance condition of an automaton are convex in the dense-time state space and use a more efficient algorithm for time progress evaluation. In fact, the restriction of location invariance condition convexity can be further relaxed to that of time-convexity for a broader range of application of the more efficient algorithm. In this work, we present techniques for the efficient model-checking of dense-time automata by taking the time-convexity of path conditions into consideration. We first identify a class of TCTL formulas that only characterize time-convex state spaces. The class includes several important types of TCTL formulas, including some timed inevitabilities with deadlines. We then present a new formulation for the efficient evaluation of timed inevitabilities with time-convex path conditions. The new formulation also leads to a new technique for the approximate evaluation of timed inevitabilities with better precision. Finally, we report our implementation and experiment.