An Improved Method to Reduce the State Space of the Timed Automata

摘要：

The timed automata is a powerful tool to model the real-time system, and the reachability of the timed automata is used to verify the safety of the real-time system. To analyze the reachability, we first expended the symbolic state generated from the conventional method, and got an improved method to generate the clock region. Then the region automaton is constructed. By traversing the predecessors and successors of the region automata, whether the given states are reachable is decided. While analyzing the reachability with our method, the state required to be traversed will much fewer. The reachability can be analyzed more quickly and fewer memories are needed. Finally, we introduced an instant to show the advantage of our method.

关键词： timed automata reachability clock region region automata symbolic state

作者: Juan Tan Yonghua Zhou Wei Han

作者单位: Center of Math Computing and Software Engineering, Zhejiang Sci-Tech University, Hangzhou, Zhejiang, P. R. China

会议类型: 国际会议

会议名称: 2010 International Conference on Circuit and Signal Processing(2010年电路与信号处理国际会议 ICCSP 2010)

会议地点: 上海

会议语种:英文

页码: 548-551

在线出版日期: 2010-12-25（万方平台首次上网日期，不代表论文的发表时间）