Study On Exact Acceleration Of Real-Time Model Checking

Different time scales do often occur in real-time systems. However, when these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. (fragmentation problem).Exact acceleration can address the fragmentation problem in the model checking when different time scales occur in real-time systems, and it does not alter reachability properties, and also can speed-up forward symbolic reachability analysis in a significant way. In this paper, we propose a new way to construct the additional cycle in the exact acceleration technique, which can resolve the problem that the size of the additional cycle depends on the window of the acceleratable cycle, and making the construction of additional cycles is more simpler and quicker. We also explore a fast method of calculating edge conditions, thus escape to compute the window of the accelerated cycle.In addition, to carry out exact acceleration, a way to identify acceleratable cycles in timed automata is proposed. Inspired by the topological sort, the method improves the efficiency to identify acceleratable cycles in timed automata by reducing the size of timed automata. The validity of this method by examples and the complexity analysis illuminate the feasibility.