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).