Checking hybrid automata for linear duration invariants

  • Li Xuandong
  • Dang Van Hung
  • Zheng Tao
Session 4
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


In this paper, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of real-time properties represented by linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for solving the problem for a class of hybrid automata.


Real-time and Hybrid Systems Model-Checking Duration Calculus Linear Programming 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.CrossRefGoogle Scholar
  2. 2.
    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
  3. 3.
    Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A Calculus of Durations. In Information Processing Letter, 40, 5, 1991, pp.269–276.CrossRefGoogle Scholar
  4. 4.
    Zhou Chaochen, Zhang Jingzhong, Yang Lu and Li Xiaoshan. Linear Duration Invariants. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, pp.88–109.Google Scholar
  5. 5.
    Rajeev Alur, David L. Dill. A theory of timed automata. In Theoretical Computer Science, 126 (1994), pp.183–235.CrossRefGoogle Scholar
  6. 6.
    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
  7. 7.
    S.C. Kleene. Representation of Events in Nerve Nets and Finite Automata. In Automata Studies, C.Shannon and J. McCarthy (eds.), Princeton Univ. Press, Princeton, NJ, 1956, pp.3–41.Google Scholar
  8. 8.
    J.U. Skakkebaek and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, pp.660–697.Google Scholar
  9. 9.
    Li Xuandong, Dang Van Hung. Checking Linear Duration Invariants by Linear Programming. In Concurrence and Parallelism, Programming, Networking, and Security, LNCS 1179, pp.321–332.Google Scholar
  10. 10.
    Li Xuandong, Dang Van Hung, Zheng Tao. Checking Hybrid Automata for Linear Duration Invariants. Research report 109, UNU/IIST, P.O.Box 3058, Macau, June 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Li Xuandong
    • 1
  • Dang Van Hung
    • 1
  • Zheng Tao
    • 1
  1. 1.International Institute for Software TechnologyThe United Nations UniversityMacau

Personalised recommendations