Folk Theorems on the Determinization and Minimization of Timed Automata

  • Stavros Tripakis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


Timed automata are known not to be complementable or determinizable. Natural questions are, then, could we check whether a given TA enjoys these properties? These problems are not algorithmically solvable, if we require not just a yes/no answer, but also a witness. Minimizing the “resources” of a TA (number of clocks or size of constants) are also unsolvable problems. Proofs are provided as simple reductions from the universality problem. These proofs are not applicable to the corresponding decision problems, the decidability of which remains open.


Fault Diagnosis Discrete State Time Automaton Folk Theorem 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. 1.
    Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D.L., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 340–354. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Alur, R., Fix, L., Henzinger, T.: A determinizable class of timed automata. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)Google Scholar
  4. 4.
    Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Expressiveness of updatable timed automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, p. 232. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)Google Scholar
  8. 8.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proc. 17th IEEE Real-Time Systems Symposium, RTSS 1996 (1996)Google Scholar
  9. 9.
    D’Souza, D., Madhusudan, P.: Controller synthesis for timed specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, p. 571. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 343. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Springintveld, J., Vaandrager, F., D’Argenio, P.: Testing timed automata. Theoretical Computer Science 254 (2001)Google Scholar
  12. 12.
    Springintveld, J.G., Vaandrager, F.W.: Minimizable timed automata. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 130–147. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Tripakis, S.: Fault diagnosis for timed automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 205. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar
  15. 15.
    Wilke, T.: Automaten und Logiken zur Beschreibung zeitabhängiger Systeme. PhD thesis, Institut Für Informatik und Praktische Mathematik, Christian- Albrechts Universität, Kiel (1994) ( in German)Google Scholar
  16. 16.
    Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. Formal Methods in System Design 11(2) (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Stavros Tripakis
    • 1
  1. 1.VERIMAG Centre EquationGièresFrance

Personalised recommendations