Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems

  • Patricia Bouyer
  • François Laroussinie
  • Pierre-Alain Reynier
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


Timed automata (TA) are a widely used model for real-time systems. Several tools are dedicated to this model, and they mostly implement a forward analysis for checking reachability properties. Though diagonal constraints do not add expressive power to classical TA, the standard forward analysis algorithm is not correct for this model. In this paper we survey several approaches to handle diagonal constraints and propose a refinement-based method for patching the usual algorithm: erroneous traces found by the classical algorithm are analyzed, and used for refining the model.


Symbolic Execution Time Automaton Clock Constraint Forward Analysis Time Automaton 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACD93]
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [AD94]
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [ADI03]
    Alur, R., Dang, T., Ivančić, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 208–223. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. [AIKY95]
    Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Information and Computation 118(1), 142–157 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  5. [BBFL03]
    Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–277. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. [BBLP05]
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelànek, R.: Zone based abstractions for timed automata exploiting lower and upper bounds. Software Tools for Technology Transfer (2005) (to appear)Google Scholar
  7. [BC05]
    Bouyer, P., Chevalier, F.: On conciseness of extensions of timed automata. Journal of Automata, Languages and Combinatorics (2005) (to appear)Google Scholar
  8. [BDGP98]
    Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36(2–3), 145–182 (1998)zbMATHMathSciNetGoogle Scholar
  9. [BLR05]
    Bouyer, P., Laroussinie, F., Reynier, P.-A.: Diagonal constraints in timed automata — Forward analysis of timed systems. Research Report LSV-05-14, Laboratoire Spécification & Vérification, ENS de Cachan, France (2005)Google Scholar
  10. [BM83]
    Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proc. IFIP 9th World Computer Congress. Information Processing, vol. 83, pp. 41–46. North-Holland/ IFIP (1983)Google Scholar
  11. [Bou03]
    Bouyer, P.: Untameable timed automata? In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. [Bou04]
    Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004)zbMATHCrossRefGoogle Scholar
  13. [BY03]
    Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491–503. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. [BY04]
    Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. [CGJ+00]
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. [Dil90]
    Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)Google Scholar
  17. [DOTY96]
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  18. [DT98]
    Daws, C., Tripakis, S.: Model-checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  19. [DY96]
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proc. 17th IEEE Real-Time Systems Symposium (RTSS 1996), pp. 73–81. IEEE Computer Society Press, Los Alamitos (1996)CrossRefGoogle Scholar
  20. [FPY02]
    Fersman, E., Petterson, P., Yi, W.: Timed automata with asynchrounous processes: Schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. [HJMS02]
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. 29th ACM Symposium on Principles of Programming Languages (POPL 2002), pp. 58–70. ACM Press, New York (2002)CrossRefGoogle Scholar
  22. [HNSY94]
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model-checking for real-time systems. Information and Computation 111(2), 193–244 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  23. [LPY97]
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Journal of Software Tools for Technology Transfer (STTT) 1(1–2), 134–152 (1997)Google Scholar
  24. [MRS02]
    Oliver Möller, M., Rueß, H., Sorea, M.: Predicate abstraction for dense real-time systems. In: Proc. Theory and Practice of Timed Systems (TPTS 2002). Electronic Notes in Theoretical Computer Science, vol. 65(6), pp. 1–20. Elsevier, Amsterdam (2002)Google Scholar
  25. [Sor04]
    Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  26. [TY01]
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Patricia Bouyer
    • 1
  • François Laroussinie
    • 1
  • Pierre-Alain Reynier
    • 1
  1. 1.LSV – CNRS & ENS CachanFrance

Personalised recommendations