Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking

When real-time systems are modeled as timed automata, different time scales may lead to a lot of fragmentations of the symbolic state space. This problem can be solved by computing the zones which in practice use the abstraction technique. The state-of-the-art abstraction methods produce an approximation that is closer to the actual reachable clock valuation, which are coarser abstractions. The exact acceleration is a finer abstraction way to reduce the required storage space and it can solve or alleviate the state space explosion problem of the fragmentations. Calculating the acceleratable cycle’s window is the key technology in exact acceleration. The calculation of the window in acceleratable cycle depends on the location invariant, edge constraint and clock reset. By comprehensively analyzing the exact acceleration principle, an algorithm is proposed to calculate the window in exact acceleration. Firstly, it is important to identify all acceleratable cycles in time automaton. Choose one node with clock reset on incoming edge as the start and check whether there is a clock reset on outgoing edge for every nodes. Secondly, all the recorded nodes link as a new cycle according to the recording ordering. Each node in new cycle has the original location invariant and each edge contains clock reset. In addition, edge constraints need to calculate. Finally, the window of acceleratable cycle can denote an interval ［a,b］, where a means the sum of edge constraints and b means the sum of location invariants. The time complexity of the algorithm is O(n\+2). According to the calculation principle, the algorithm can get the valid data of the window, reduce other useless data and nodes, compress the acceleratable cycle, make the model simpler and enhance the computing efficiency. The algorithm lays the foundation for the research and development of the automatic model checking program.