Some progress in the symbolic verification of timed automata

  • Marius Bozga
  • Oded Maler
  • Amir Pnueli
  • Sergio Yovine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


In this paper we discuss the practical difficulty of analyzing the behavior of timed automata and report some results obtained using an experimental BDD-based extension of KRONOS. We have treated examples originating from timing analysis of asynchronous boolean networks and CMOS circuits with delay uncertainties and the results outperform those obtained by previous implementations of timed automata verification tools.


Reachable State Timing Verification Time Automaton Asynchronous Circuit Time Transition System 
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. [AD94]
    R. Alur and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.Google Scholar
  2. [ACD93]
    R. Alur, C. Courcoubetis, and D.L. Dill, Model Checking in Dense Real Time, Information and Computation 104, 2–34, 1993.Google Scholar
  3. [AH92]
    R. Alur and T.A. Henzinger, Logics and Models for Real-Time: A survey, J.W. de Bakker et al (Eds.), Real-Time: Theory in Practice, LNCS 600, 74–106, Springer, 1992.Google Scholar
  4. [AIKY95]
    R. Alur, A. Itai, R.P. Kurshan and M. Yanakakis, Timing Verification by Successive Approximation, Information and Computation 118, 142–157, 1995.Google Scholar
  5. [AK96]
    R. Alur, and R.P. Kurshan, Timing Analysis in COSPAN, in R. Alur, T.A. Henzinger and E. Sontag (Eds.), Hybrid Systems III, LNCS 1066, 220–231, Springer, 1996.Google Scholar
  6. [ABK+97]
    E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli and A. Rasse, Data-Structures for the Verification of Timed Automata, in O. Maler (Ed.), Proc. HART'97, LNCS 1201, 346–360, Springer, 1997.Google Scholar
  7. [ACM96]
    E. Asarin, P. Caspi and O. Maler, A Kleene Theorem for Timed Automata, Proc. LICS'97, 1997.Google Scholar
  8. [AMP95]
    E. Asarin, O. Maler and A. Pnueli, Symbolic Controller Synthesis for Discrete and Timed Systems, in P. Antsaklis et al (Eds.), Hybrid Systems II, LNCS 999, 1–20, Springer, 1995.Google Scholar
  9. [B96]
    F. Balarin, Approximate Reachability Analysis of Timed Automata, Proc. RTSS'96, 52–61, IEEE, 1996.Google Scholar
  10. [BD91]
    B. Berthomieu and M. Diaz, Modeling and Verification of Time Dependent Systems using Time Petri Nets, IEEE Trans. on Software Engineering 17, 259–273, 1991.Google Scholar
  11. [BFK96]
    M. Bozga, J.-C. Fernandez and A. Kerbrat, A Symbolic μ-calculus Model Checker for Automata with Variables, Unpublished Manuscript, Verimag, 1996. Scholar
  12. [Bry86]
    R.E. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers C-35, 677–691, 1986.Google Scholar
  13. [BS94]
    J.A. Brzozowski and C-J.H. Seger, Asynchronous Circuits, Springer, 1994.Google Scholar
  14. [BCM+93]
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, Symbolic Model-Checking: 1020 States and Beyond, Proc. LICS'90, Philadelphia, 1990.Google Scholar
  15. [CC95]
    S.V. Campos and E.M. Clarke, Real-time Symbolic Model Checking for Discrete Time Models, in T. Rus and C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, World Scientific, 1995.Google Scholar
  16. [DOTY96]
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine, The Tool KRONOS, in R. Alur, T.A. Henzinger and E. Sontag (Eds.), Hybrid Systems III, LNCS 1066, 208–219, Springer, 1996.Google Scholar
  17. [DOY94]
    C. Daws, A. Olivero and S. Yovine, Verifying et-lotos Programs with kronos, Proc. FORTE'94, Bern, 1994.Google Scholar
  18. [DY95]
    C. Daws and S. Yovine, Two Examples of Verification of Multirate Timed Automata with KRONOS, Proc. RTSS'95, 66–75, IEEE, 1995.Google Scholar
  19. [DY96]
    C. Daws and S. Yovine, Reducing the Number of Clock Variables of Timed Automata, Proc. RTSS'96, 73–81, IEEE, 1996.Google Scholar
  20. [D89]
    D.L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, in J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems, LNCS 407, 197–212, Springer, 1989.Google Scholar
  21. [GPV94]
    A. Göllü, A. Puri and P. Varaiya, Discretization of Timed Automata, Proc. 33rd CDC, 1994.Google Scholar
  22. [H93]
    N. Halbwachs, Delay Analysis in Synchronous Programs, in C. Courcoubetis (Ed.), Proc. CAV'93, LNCS 697, 333–346, Springer, 1993.Google Scholar
  23. [HMP92a]
    T. Henzinger, Z. Manna, and A. Pnueli, Timed Transition Systems, in J.W. de Bakker et al (Eds.), Real-Time: Theory in Practice, LNCS 600, 226–251, Springer, 1992.Google Scholar
  24. [HMP92]
    T. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital Clocks?, in W. Kuich (Ed.), Proc. ICALP'92, LNCS 623, 545–558, Springer, 1992.Google Scholar
  25. [HNSY94]
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Modelchecking for Real-time Systems, Information and Computation 111, 193–244, 1994.Google Scholar
  26. [LPY95]
    K.G. Larsen, P. Pettersson and W. Yi, Compositional and Symbolic Model-Checking of Real-time Systems, Proc. RTSS'95, 76–87, IEEE, 1995.Google Scholar
  27. [L89]
    H.R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989.Google Scholar
  28. [MP95]
    O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, in P.E. Camurati, H. Eveking (Eds.), Proc. CHARME'95, LNCS 987, 189–205, Springer, 1995.Google Scholar
  29. [MY96]
    O. Maler and S. Yovine. Hardware Timing Verification using KRONOS, In Proc. 7th Israeli Conference on Computer Systems and Software Engineering, Herzliya, Israel, June 1996.Google Scholar
  30. [McM93]
    K.L. McMillan, Symbolic Model-Checking: an Approach to the State-Explosion problem, Kluwer, 1993.Google Scholar
  31. [NS92]
    X. Nicollin and J. Sifakis, An Overview and Synthesis of Timed Process Algebra, in J.W. de Bakker et al (Eds.), Real-Time.: Theory in Practice, LNCS 600, 526–548, Springer, 1992.Google Scholar
  32. [S95]
    F. Somenzi, CUDD: CU Decision Diagram Package, 1995.Google Scholar
  33. [WD94]
    H. Wong-Toi and D.L. Dill, Approximations for Verifying Timing Properties, in T. Rus and C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, World Scientific Publishing, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Marius Bozga
    • 1
  • Oded Maler
    • 1
  • Amir Pnueli
    • 2
  • Sergio Yovine
    • 1
  1. 1.Centre EquationVerimagGièresFrance
  2. 2.Dept. of Computer ScienceWeizmann Inst.RehovotIsrael

Personalised recommendations