Advertisement

The Power of Reachability Testing for Timed Automata

  • Luca Aceto
  • Patricia Bouyer
  • Augusto Burgueño
  • Kim G. Larsen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1530)

Abstract

In this paper we provide a complete characterization of the class of properties of (networks of) timed automata for which model checking can be reduced to reachability checking in the context of testing automata.

Keywords

Model Check Extended State Parallel Composition Urgent Action Time Assignment 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata (1998) (Forthcoming paper)Google Scholar
  2. 2.
    Aceto, L., Burgueño, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Burgueño, A.: Model-checking via Testing and Parametric Analysis of Timed Systems, PhD thesis, École Nationale Supérieure de l’Aéronautique et de l’Éspace, Toulouse, France (June 1998)Google Scholar
  5. 5.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: the next generation. In: Proc. of the 16th Real-time Systems Symposium, RTSS 1995. IEEE Computer Society press, Los Alamitos (1995)Google Scholar
  6. 6.
    Laroussinie, F., Larsen, K.G.: Compositional model checking of real time systems. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962. Springer, Heidelberg (1995)Google Scholar
  7. 7.
    Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic – and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)Google Scholar
  8. 8.
    Larsen, K.G., Pettersson, P., Wang, Y.: Uppaal in a nutshell. Software Tools for Technology Transfer 1, 134–152 (1997)zbMATHCrossRefGoogle Scholar
  9. 9.
    Wang, Y.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Luca Aceto
    • 1
  • Patricia Bouyer
    • 2
  • Augusto Burgueño
    • 3
  • Kim G. Larsen
    • 1
  1. 1.BRICS – Basic Research in Computer Science, Centre of the Danish National Research Foundation., Department of Computer ScienceAalborg UniversityAalborg ØDenmark
  2. 2.Laboratoire Spécification et VérificationCNRS URA 2236 Ecole Normale Supérieure de CachanCachan CedexFrance
  3. 3.ONERA-CERT, Département d’InformatiqueToulouse Cedex 4France

Personalised recommendations