Verification for Timed Automata Extended with Unbounded Discrete Data Structures

  • Karin Quaas
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this paper is to identify subclasses of timed pushdown automata for which the language inclusion problem and related problems are decidable.


Reachability Problem Input Alphabet Model Check Problem Time Automaton Clock Constraint 
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.
    Abdulla, P.A., Cerans, K.: Simulation is decidable for one-counter nets (extended abstract). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 253–268. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Deneux, J., Ouaknine, J., Quaas, K., Worrell, J.: Universality analysis for one-clock timed automata. Fundam. Inform. 89(4), 419–450 (2008)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Adams, S., Ouaknine, J., Worrell, J.B.: Undecidability of universality for timed automata with minimal resources. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 25–37. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202–211. ACM (2004)Google Scholar
  7. 7.
    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.) Hybrid Systems II. LNCS, vol. 999, pp. 64–85. Springer, Heidelberg (1995)Google Scholar
  8. 8.
    Bouchy, F., Finkel, A., Sangnier, A.: Reachability in timed counter systems. Electr. Notes Theor. Comput. Sci. 239, 167–178 (2009)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 61–70. ACM (2010)Google Scholar
  10. 10.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Bouyer, P., Larsen, K.G., Markey, N.: Lower-bound-constrained runs in weighted timed automata. Perform. Eval. 73, 91–109 (2014)CrossRefGoogle Scholar
  12. 12.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Brázdil, T., Jančar, P., Kučera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Dang, Z.: Pushdown timed automata: a binary reachability characterization and safety verification. Theor. Comput. Sci. 302(1-3), 93–121 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)Google Scholar
  16. 16.
    Demri, S., Lazić, R.S., Sangnier, A.: Model checking Freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 490–504. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. 35, 413–422 (1913)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    Ésik, Z., Fahrenberg, U., Legay, A., Quaas, K.: Kleene algebras and semimodules for energy problems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 102–117. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  20. 20.
    Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95–115. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)CrossRefzbMATHMathSciNetGoogle Scholar
  22. 22.
    Greibach, S.A.: An infinite hierarchy of context-free languages. J. ACM 16(1), 91–106 (1969)CrossRefzbMATHMathSciNetGoogle Scholar
  23. 23.
    Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society 2, 236–366 (1952)MathSciNetGoogle Scholar
  24. 24.
    Hofman, P., Lasota, S., Mayr, R., Totzke, P.: Simulation over one-counter nets is PSPACE-complete. In: Seth, A., Vishnoi, N.K. (eds.) FSTTCS. LIPIcs, vol. 24, pp. 515–526. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  25. 25.
    Hofman, P., Totzke, P.: Trace inclusion for one-counter nets revisited. CoRR, abs/1404.5157 (2014)Google Scholar
  26. 26.
    Ibarra, O.H.: Restricted one-counter machines with undecidable universe problems. Mathematical Systems Theory 13, 181–186 (1979)CrossRefzbMATHMathSciNetGoogle Scholar
  27. 27.
    Jančar, P., Esparza, J., Moller, F.: Petri nets and regular processes. J. Comput. Syst. Sci. 59(3), 476–503 (1999)CrossRefzbMATHGoogle Scholar
  28. 28.
    Jančar, P., Kucera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput. 188(1), 1–19 (2004)CrossRefzbMATHGoogle Scholar
  29. 29.
    Juhl, L., Guldstrand Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) He Festschrift. LNCS, vol. 8051, pp. 244–255. Springer, Heidelberg (2013)Google Scholar
  30. 30.
    Information Sciences Institute of the University of Southern California. Transmission Control Protocoll (DARPA Internet Program Protocol Specification) (1981),
  31. 31.
    Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: LICS, pp. 54–63. IEEE Computer Society (2004)Google Scholar
  32. 32.
    Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS, pp. 188–197. IEEE Computer Society (2005)Google Scholar
  33. 33.
    Ouaknine, J., Worrell, J.B.: On metric temporal logic and faulty turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  34. 34.
    Quaas, K.: On the interval-bound problem for weighted timed automata. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 452–464. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  35. 35.
    Quaas, K.: Model checking metric temporal logic over automata with one counter. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 468–479. Springer, Heidelberg (2013)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Karin Quaas
    • 1
  1. 1.Universität LeipzigGermany

Personalised recommendations