Advertisement

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

  • Li Xuandong
  • Pei Yu
  • Zhao Jianhua
  • Li Yong
  • Zheng Tao
  • Zheng Guoliang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)

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.

References

  1. 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. 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
  3. 3.
    R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. In Theoretical Computer Science, 138(1995), pp. 3–34.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s Decidable About Hybrid Automata? In Journal of Computer and System Sciences, 57:94–124, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A Calculus of Durations. In Information Processing Letter, 40,5, 1991, pp. 269–276.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 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. 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
  8. 8.
    T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: a model checker for hybrid systems. In Software Tools for Technology Transfer, 1:110–122, 1997.zbMATHCrossRefGoogle Scholar
  9. 9.
    Li Xuandong, Dang Van Hung, and Zheng Tao. Checking Hybrid Automata for Linear Duration Invariants. In Advances in Computing Science-ASIAN’97, LNCS 1345, Springer-Verlag, 1997, pp. 166–1180.CrossRefGoogle Scholar
  10. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Li Xuandong
    • 1
  • Pei Yu
    • 1
  • Zhao Jianhua
    • 1
  • Li Yong
    • 1
  • Zheng Tao
    • 1
  • Zheng Guoliang
    • 1
  1. 1.State Key Laboratory of Novel Software Technology Department of Computer Science and TechnologyNanjing UniversityNanjing JiangsuP.R. China

Personalised recommendations