Exact Acceleration of Real-Time Model Checking Based on Parking Cycle
Wang Cong-yin · Dianzi xuebao · 2011
Different time scales are often found between control systems and their environments.When these systems are modeled as timed automata,such difference can lead to fragmentation of the symbolic state space in the process of applying symbolic model checking techniques to the validation of them.Exact acceleration addresses the fragmentation problem without any side-effect to the reachability properties of the system under consideration.To address the fragmentation problems caused by the acceleratable cycles,this paper introduces an exact acceleration technique based on parking cycle.The length of the parking cycle is constant,without dependency on the window of the acceleratable cycles,and so makes the constructed acceleration simpler,the process of the exact acceleration faster,and both the time cost and the space cost of exact acceleration can be greatly reduced.