Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming
In this paper, we show that for a class of linear hybrid automata called zero loop-closed automata, the satisfaction problem for linear duration properties can be solved efficiently by linear programming. We give an algorithm based on depth-first search method to solve the problem by traversing all the simple paths (with no repeated node occurrence) in an automaton and checking their corresponding sequences of locations for a given linear duration property.
- 1.Thomas A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292.Google Scholar
- 2.Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Hybrid System, LNCS 736, pp. 179–208.Google Scholar
- 6.C. Zhou, J. Zhang, L. Yang, and X. Li. Linear Duration Invariants. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, pp. 88–109.Google Scholar
- 7.Thomas A. Henzinger, Rupak Majumdar. Symbolic Model Checking for Rectangular Hybrid Systems. In Proceedings of the Sixth Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 00), Lecture Notes in Computer Science, Springer, 2000.Google Scholar
- 10.Li Xuandong, Zheng Tao, Hou Jianmin, Zhao Jianhua, and Zheng Guoliang. Hybrid Regular Expressions. In Hybrid Systems: Computation and Control, LNCS 1386, Springer-Verlag, 1998, pp. 384–399.Google Scholar