关键词: 线性混成自动机, 迁移系统, 安全性验证, 不变式生成

Abstract: The behavior of hybrid system is very complex. It consists of both discrete transition and continuous timed behavior. Therefore, the safety verification of hybrid automata is very difficult. Even for the class of linear hybrid automata, the reachability verification problem is undecidable. Most existing techniques compute the state space of linear hybrid automata through polyhedral computation, which is not suitable for large scale system. This paper presents a new tool to transform the linear hybrid automata into an equivalent transition system. Then, this tool can use the invariant generation studies on transition system to answer the reachability problem of linear hybrid automata. The experimental results indicate that the performance of this tool is nice and it can be applied to large systems.

Key words: linear hybrid antomata, transition system, safety verification, invariant generation