Event-Clock Nested Automata

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10792)


In this paper we introduce and study Event-Clock Nested Automata (ECNA), a formalism that combines Event Clock Automata (ECA) and Visibly Pushdown Automata (VPA). ECNA allow to express real-time properties over non-regular patterns of recursive programs. We prove that ECNA retain the closure and decidability properties of ECA and VPA being closed under Boolean operations and having a decidable language-inclusion problem. In particular, we prove that emptiness, universality, and language-inclusion for ECNA are Exptime-complete problems. As for the expressiveness, we have that ECNA properly extend any previous attempt in the literature of combining ECA and VPA.


  1. 1.
    Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: Proceedings of 27th LICS, pp. 35–44. IEEE Computer Society (2012)Google Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefMATHGoogle Scholar
  3. 3.
    Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24730-2_35 CrossRefGoogle Scholar
  4. 4.
    Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theoret. Comput. Sci. 211(1–2), 253–273 (1999)MathSciNetCrossRefMATHGoogle Scholar
  5. 5.
    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of 36th STOC, pp. 202–211. ACM (2004)Google Scholar
  6. 6.
    Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1–16:43 (2009)Google Scholar
  7. 7.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)Google Scholar
  8. 8.
    Benerecetti, M., Peron, A.: Timed recursive state machines: expressiveness and complexity. Theoret. Comput. Sci. 625, 85–124 (2016)MathSciNetCrossRefMATHGoogle Scholar
  9. 9.
    Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A logical characterization for dense-time visibly pushdown automata. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 89–101. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30000-9_7 CrossRefGoogle Scholar
  10. 10.
    Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 64–85. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60472-3_4 CrossRefGoogle Scholar
  11. 11.
    Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 504–518. Springer, Heidelberg (2005).  https://doi.org/10.1007/11591191_35 CrossRefGoogle Scholar
  12. 12.
    Bozzelli, L., Murano, A., Peron, A.: Event-clock nested automata (2017). http://arxiv.org/abs/1711.08314
  13. 13.
    Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack size analysis for interrupt-driven programs. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 109–126. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_7 CrossRefGoogle Scholar
  14. 14.
    Clemente, L., Lasota, S.: Timed pushdown automata revisited. In: Proceedings of 30th LICS, pp. 738–749. IEEE Computer Society (2015)Google Scholar
  15. 15.
    Emmi, M., Majumdar, R.: Decision problems for the verification of real-time software. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 200–211. Springer, Heidelberg (2006).  https://doi.org/10.1007/11730637_17 CrossRefGoogle Scholar
  16. 16.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 262–277. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36078-6_18 CrossRefGoogle Scholar
  17. 17.
    Murano, A., Perelli, G.: Pushdown multi-agent system verification. In: Proceedings of IJCAI, pp. 1090–1097 (2015)Google Scholar
  18. 18.
    Van Tang, N., Ogawa, M.: Event-clock visibly pushdown automata. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 558–569. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-540-95891-8_50 CrossRefGoogle Scholar
  19. 19.
    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).  https://doi.org/10.1007/978-3-642-15643-4_23 CrossRefGoogle Scholar
  20. 20.
    Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61474-5_58 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Università degli Studi di Napoli Federico IINaplesItaly

Personalised recommendations