Lecture Notes in Computer Science, 2001, Volume 2144/2001, 465-479, DOI: 10.1007/3-540-44798-9_35

Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming

Li Xuandong, Pei Yu, Zhao Jianhua, Li Yong, Zheng Tao and Zheng Guoliang

View Related Documents

Abstract

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.
This work is supported by the National Natural Science Foundation of China under Grant 60073031 and Grant 69703009, and by International Institute for Software Technology, The United Nations University (UNU/IIST).

Fulltext Preview

Image of the first page of the fulltext document