Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics

  • Marius Bozga
  • Oded Maler
  • Stavros Tripakis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


In this paper we argue that the semantic issues of discrete vs. dense time should be separated as much as possible from the pragmatics of state-space representation. Contrary to some misconceptions, the discrete semantics is not inherently bound to use state-explosive techniques any more than the dense one. In fact, discrete timed automata can be analyzed using any representation scheme (such as DBM) used for dense time, and in addition can benefit from enumerative and symbolic techniques (such as BDDs) which are not naturally applicable to dense time. DBMs, on the other hand, can still be used more efficiently by taking into account the activity of clocks, to eliminate redundancy. To support these claims we report experimental results obtained using an extension of Kronos with BDDs and variable-dimension DBMs where we verified the asynchronous chip STARI, a FIFO buffer which provides for skew-tolerant communication between two synchronous systems. Using discrete time and BDDs we were able to prove correctness of a STARI implementation with 18 stages (55 clocks), better than what has been achieved using other techniques. The verification results carry over to the dense semantics.

Using variable-dimension DBMs we have managed to verify STARI for up to 8 stages (27 clocks). In fact, our analysis shows that at most one third of the clocks are active at any reachable state, and about one fourth of the clocks are active in 90% of the reachable states.


  1. AD94.
    R. Alur and D. L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.Google Scholar
  2. 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.CrossRefGoogle Scholar
  3. 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.CrossRefGoogle Scholar
  4. 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
  5. AMP98.
    E. Asarin, O. Maler and A. Pnueli, On the Discretization of Delays in Timed Automata and Digital Circuits, in R. de Simone and D. Sangiorgi (Eds), Proc. Concur’98, LNCS 1466, 470–484, Springer, 1998.Google Scholar
  6. B96.
    F. Balarin, Approximate Reachability Analysis of Timed Automata, Proc. RTSS’96, 52–61, IEEE, 1996.Google Scholar
  7. B97.
    M. Bozga, SMI: An Open Toolbox for Symbolic Protocol Verification, Technical Report 97-10, Verimag, 1997.
  8. BM98.
    W. Belluomini and C. J. Myers, Verification of Timed Systems Using POSETs, in A. J. Hu and M. Y. Vardi (Eds.), Proc. CAV’98, 403–415, LNCS 1427, Springer, 1997.Google Scholar
  9. BMPY97.
    M. Bozga, O. Maler, A. Pnueli, S. Yovine, Some Progress in the Symbolic Verification of Timed Automata, in O. Grumberg (Ed.) Proc. CAV’97, 179–190, LNCS 1254, Springer, 1997.Google Scholar
  10. BS94.
    J. A. Brzozowski and C-J. H. Seger, Asynchronous Circuits, Springer, 1994.Google Scholar
  11. 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.CrossRefGoogle Scholar
  12. DT98.
    C. Daws and S. Tripakis, Model checking of Real-time Reachability Properties using Abstractions, Proc. TACAS’98, LNCS 1384, 1998.Google Scholar
  13. DY96.
    C. Daws and S. Yovine, Reducing the Number of Clock Variables of Timed Automata, Proc. RTSS’96, 73–81, IEEE, 1996.Google Scholar
  14. 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
  15. FKM93.
    J. C. Fernandez, A. Kerbrat, and L. Mounier, Symbolic Equivalence Checking, In C. Courcoubetis (Ed.), Proc. CAV’93, LNCS 697, Springer, 1993.Google Scholar
  16. Gre97.
    M. R. Greenstreet, STARI: Skew Tolerant Communication, to appear in IEEE Transactions on Computers, 1997.Google Scholar
  17. H93.
    N. Halbwachs, Delay Analysis in Synchronous Programs, in C. Courcoubetis (Ed.), Proc. CAV’93, LNCS 697, 333–346, Springer, 1993.Google Scholar
  18. 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
  19. LLPY97.
    K. Larsen, F. Larsson, P. Pettersson and W. Yi, Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction, Proc. RTSS’98, 14–24, 1997.Google Scholar
  20. LPY97.
    K. G. Larsen, P. Pettersson and W. Yi, UPPAAL in a Nutshell, Software Tools for Technology Transfer 1/2, 1997.Google Scholar
  21. L89.
    H. R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989.Google Scholar
  22. 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
  23. S95.
    F. Somenzi, CUDD: CU Decision Diagram Package, 1995.Google Scholar
  24. SV96.
    J. Springintveld and F. W. Vaandrager, Minimizable Timed Automata, in B. Jonsson and J. Parrow (Eds.), Proc. FTRTFT’96, LNCS 1135, 130–147, Springer, 1996.Google Scholar
  25. TAKB96.
    S. Tasiran R. Alur, R. P. Kurshan and R. Brayton, Verifying Abstractions of Timed Systems, in Proc. CONCUR’96, 546–562, Springer, 1996.Google Scholar
  26. TB97.
    S. Tasiran and R. K. Brayton, STARI: A Case Study in Compositional and Hierarchical Timing Verification, in O. Grumberg (Ed.) Proc. CAV’97, 191–201, LNCS 1254, Springer, 1997.Google Scholar
  27. TKB97.
    S. Tasiran, Y. Kukimoto and R. K. Brayton, Computing Delay with Coupling using Timed Automata, Proc. TAU’97, 1997.Google Scholar
  28. vGW89.
    R. J. van Glabbeek and W. P. Weijland, Branching-Time and Abstraction in Bisimulation Semantics (extended abstract), CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989.Google Scholar
  29. 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
  30. YR99.
    T. Yoneda and H. Ryu, Timed Trace Theoretic Verification Using Partial Order Reductions, in Proc. Async’99, 108–121, IEEE Press, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Marius Bozga
    • 1
  • Oded Maler
    • 1
  • Stavros Tripakis
    • 1
  1. 1.VerimagCentre EquationGièresFrance

Personalised recommendations