Reducing Clocks in Timed Automata while Preserving Bisimulation

  • Shibashis Guha
  • Chinmay Narayan
  • S. Arun-Kumar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.


Model Check Chromatic Number Outgoing Edge Incoming Edge Base Zone 
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.
    Aceto, L., Ing\(\acute{o}\)lfsd\(\acute{o}\)ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press (2007)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation 104, 2–34 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    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–270. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelanek, R.: Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer 8, 204–215 (2006)CrossRefGoogle Scholar
  6. 6.
    Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time petri nets. In: IFIP Congress, pp. 41–46 (1983)Google Scholar
  7. 7.
    Čerāns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: IEEE Proc. RTSS 1996, pp. 73–81. IEEE Computer Society Press (1996)Google Scholar
  10. 10.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  11. 11.
    Eppstein, D.: Small maximal independent sets and faster exact graph coloring. Journal of Graph Algorithms and Applications 7, 131–140 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Finkel, O.: Undecidable problems about timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 187–199. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Guha, S., Krishna, S.N., Narayan, C., Arun-Kumar, S.: A unifying approach to decide relations for timed automata and their game characterization. In: Express/SOS, pp. 47–62 (2013)Google Scholar
  14. 14.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-time Systems. In: Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS 1992), Santa Cruz, California, USA, June 22-25, pp. 394–406. IEEE Computer Society (1992)Google Scholar
  15. 15.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: The Proceedings of Logic in Computer Science, LICS (1992)Google Scholar
  16. 16.
    Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic – and back. In: Wiedermann, J., Hájek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  17. 17.
    Laroussinie, F., Schnoebelen, P.: The state explosion problem from trace to bisimulation equivalence. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 192–207. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Lawler, E.L.: A note on the complexity of the chromatic number problem. Information Processing Letters 5, 66–67 (1976)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Tripakis, S.: Folk theorems on the determinization and minimization of timed automata. Information Processing Letters 99, 222–226 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18, 25–68 (2001)CrossRefzbMATHGoogle Scholar
  21. 21.
    Weise, C., Lenzkes, D.: Efficient scaling-invariant checking of timed bisimulation. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 177–188. Springer, Heidelberg (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Shibashis Guha
    • 1
  • Chinmay Narayan
    • 1
  • S. Arun-Kumar
    • 1
  1. 1.Indian Institute of Technology DelhiNew DelhiIndia

Personalised recommendations