Verifying ω-regular properties for a subclass of linear hybrid systems

  • Ahmed Bouajjani
  • Riadh Robbana
Session 12: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We address the problem of verifying untimed ω-regular properties for a subclass of linear hybrid systems, i.e., finite transition graphs supplied with real-valued variables that change continuously with integer rates at each control location. The systems we consider are systems with two variables, one of them must be monotonic (e.g., with rates either 0 or 1) whereas the other one can have rates either −1, 0, or 1. We prove that for these systems, the verification problem of ω-regular properties is decidable. For that, we show that these systems generate ω-context-free sets of state sequences.


Hybrid System Temporal Logic State Sequence Transition Graph Atomic Proposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In LICS'90. IEEE, 1990.Google Scholar
  2. 2.
    R. Alur, C. Courcoubetis, T. Henzinger, and P-H. Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  3. 3.
    E. Asarin, O. Maler, and A. Pnueli. Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives. T.C.S., 138, 1995.Google Scholar
  4. 4.
    Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40:269–276, 1991.Google Scholar
  5. 5.
    E. Clarke, A. Emerson, and P. Sistla. Automatic Verification of Finite State Con-current Systems using Temporal Logic Specifications: A Practical Approach. In POPL'83, 1983.Google Scholar
  6. 6.
    R.S. Cohen and A.Y. Gold. Theory of ω-Languages. I: Characterizations of ω-Context-Free Languages. J.C.S.S., 15:169–184, 1977.Google Scholar
  7. 7.
    E.Clarke, O. Grümberg, and R. Kurshan. A Synthesis of two Approaches for Verifying Finite State Concurrent Systems. In CMU tech. rep., 1987.Google Scholar
  8. 8.
    E.A. Emerson and J. Y. Halpern. 'sometimes’ and’ Not Never’ Revisited: On Branching vs. Linear Time Logic. In POPL'83, 1983.Google Scholar
  9. 9.
    T. Henzinger. Hybrid Automata with Finite Bisimulations. In ICALP'95, 1995.Google Scholar
  10. 10.
    T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's Decidable about Hybrid Automata. In STOC'95, 1995.Google Scholar
  11. 11.
    Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  12. 12.
    O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In REX workshop on Real-Time: Theory and Practice. LNCS 600, 1992.Google Scholar
  13. 13.
    D.E. Muller. Infinite Sequences and Finite Machines. In 4th Symp. on Switching Circuit Theory and Logical Design. IEEE, 1963.Google Scholar
  14. 14.
    X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An Approach to the Description and Analysis of Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  15. 15.
    A. Pnueli. The Temporal Logic of Programs. In FOCS'77. IEEE, 1977.Google Scholar
  16. 16.
    W. Thomas. Computation Tree Logic and Regular ω-Languages. LNCS 354, 1989.Google Scholar
  17. 17.
    W. Thomas. Automata on Infinite Objects. In Handbook of Theo. Comp. Sci. Elsevier Sci. Pub., 1990.Google Scholar
  18. 18.
    M.Y. Vardi. A Temporal Fixpoint Calculus. In POPL'88, 1988.Google Scholar
  19. 19.
    P. Wolper. Temporal Logic Can Be More Expressive. Inform. and Cont., 56, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ahmed Bouajjani
    • 1
  • Riadh Robbana
    • 1
  1. 1.Verimag, Miniparc-ZirstMontbonnot St-MartinFrance

Personalised recommendations