Nested Timed Automata

  • Guoqiang Li
  • Xiaojuan Cai
  • Mizuhito Ogawa
  • Shoji Yuen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)


This paper proposes a new timed model named nested timed automata (NeTAs). A NeTA is a pushdown system whose stack symbols are timed automata (TAs). It either behaves as the top TA in the stack, or switches from one TA to another by pushing, popping, or changing the top TA of the stack. Different from existing component-based context-switch models such as recursive timed automata and timed recursive state machines, when time passage happens, all clocks of TAs in the stack elapse uniformly. We show that the safety property of NeTAs is decidable by encoding NeTAs to the dense timed pushdown automata. NeTAs provide a natural way to analyze the recursive behaviors of component-based timed systems with structure retained. We illustrate this advantage by the deadline analysis of nested interrupts.


Safety Property State Reachability Discrete Transition Context Switch Local Clock 
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., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Bouajjani, A., Echahed, R., Robbana, R.: On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 64–85. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-Timed Pushdown Automata. In: Proceedings of the LICS 2012, pp. 35–44. IEEE Computer Society (2012)Google Scholar
  4. 4.
    Trivedi, A., Wojtczak, D.: Recursive Timed Automata. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 306–324. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Benerecetti, M., Minopoli, S., Peron, A.: Analysis of Timed Recursive State Machines. In: Proceedings of the TIME 2010, pp. 61–68. IEEE Computer Society (2010)Google Scholar
  6. 6.
    Li, G., Cai, X., Ogawa, M., Yuen, S.: Nested Timed Automata. Technical Report IS-RR-2013-004, JAIST (2013)Google Scholar
  7. 7.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. Information and Computation 111, 193–244 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Ogawa, M., Cai, X.: On Reachability of Dense Timed Pushdown Automata. Technical Report IS-RR-2013-005, JAIST (2013)Google Scholar
  9. 9.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable Timed Automata. Theoretical Computer Science 321, 291–345 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    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
  11. 11.
    Li, G., Yuen, S., Adachi, M.: Environmental Simulation of Real-Time Systems with Nested Interrupts. In: Proceedings of the TASE 2009, pp. 21–28. IEEE Computer Society (2009)Google Scholar
  12. 12.
    Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-Driven Software. IEEE Transactions on Software Engineering (TSE) 30, 634–655 (2004)CrossRefGoogle Scholar
  13. 13.
    Fersman, E., Krcal, P., Pettersson, P., Yi, W.: Task Automata: Schedulability, Decidability and Undecidability. Information and Computation 205, 1149–1172 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Dang, Z.: Pushdown Timed Automata: A Binary Reachability Characterization and Safety Verification. Theoretical Computer Science 302, 93–121 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    Abdulla, P.A., Atig, M.F., Stenman, J.: The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 58–69. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  16. 16.
    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of Recursive State Machines. ACM Transactions on Programming Languages and Systems (TOPLAS) 27, 786–818 (2005)CrossRefGoogle Scholar
  17. 17.
    David, A., Möller, M.O.: From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata. Technical Report RS-01-11, BRICS (2001)Google Scholar
  18. 18.
    Li, G., Cai, X., Yuen, S.: Modeling and Analysis of Real-Time Systems with Mutex Components. International Journal of Foundations of Computer Science (IJFCS) 23, 831–851 (2012)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Guoqiang Li
    • 1
  • Xiaojuan Cai
    • 1
  • Mizuhito Ogawa
    • 2
  • Shoji Yuen
    • 3
  1. 1.School of SoftwareShanghai Jiao Tong UniversityChina
  2. 2.Japan Advanced Institute of Science and TechnologyJapan
  3. 3.Graduate School of Information ScienceNagoya UniversityJapan

Personalised recommendations