YIN Chuan-long, ZHUANG Lei, WANG Cong-yin. Exact Acceleration of Real-Time Model Checking Based on Parking Cycle[J]. Acta Electronica Sinica, 2011, 39(3): 489-493.
DOI:
YIN Chuan-long, ZHUANG Lei, WANG Cong-yin. Exact Acceleration of Real-Time Model Checking Based on Parking Cycle[J]. Acta Electronica Sinica, 2011, 39(3): 489-493.DOI:
Exact Acceleration of Real-Time Model Checking Based on Parking Cycle
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.