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

摘要： 混成自动机行为中既包含离散行为又包含连续行为，非常复杂。其安全性验证问题难以解决，即使是线性混成自动机，它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集，复杂度高，可处理问题规模非常有限。为了避免这类问题，实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统，并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明，方法有效可行，工具具有良好的性能。

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