Abstract
We investigate reachability in pushdown automata over infinite alphabets: machines with finite control, a finite collection of registers and pushdown stack. First we show that, despite the stack’s unbounded storage capacity, in terms of reachability/emptiness these machines can be faithfully represented by using only 3r elements of the infinite alphabet, where r is the number of registers. Moreover, this bound is tight. Next we settle the complexity of the associated reachability/emptiness problems. In contrast to register automata, where differences in register storage policies gave rise to differing complexity bounds, the emptiness problem for pushdown register automata is EXPTIME-complete in all cases. We also provide a solution to the global reachability problem, based on representing pushdown configurations with a special register automaton. Finally, we examine extensions of pushdown storage to higher orders and show that reachability is undecidable already at order 2, unlike in the finite alphabet case.
Research supported by the Engineering and Physical Sciences Research Council (EP/J019577/1) and the Royal Academy of Engineering (RF: Tzevelekos).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Cerný, P., Weinstein, S.: Algorithmic analysis of array-accessing programs. ACM Trans. Comput. Log. 13(3) (2012)
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. Log. Meth. Comput. Sci. 7(4) (2011)
Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4-5) (2010)
Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4) (2011)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207–220. Springer, Heidelberg (2007)
Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. Theor. Comput. Sci. 295, 85–106 (2003)
Cheng, E.Y.C., Kaminski, M.: Context-free languages over infinite alphabets. Acta Inf. 35(3), 245–267 (1998)
Cook, S.A.: Characterizations of pushdown machines in terms of time-bounded computers. J. ACM 18(1), 4–18 (1971)
Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13 (2002)
Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260–276. Springer, Heidelberg (2013)
Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2) (1994)
Kaminski, M., Zeitlin, D.: Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci. 21(5) (2010)
Maslov, A.N.: Multilevel stack automata. Probl. of Inf. Transm. 12 (1976)
Murawski, A.S., Tzevelekos, N.: Algorithmic nominal game semantics. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 419–438. Springer, Heidelberg (2011)
Murawski, A.S., Tzevelekos, N.: Algorithmic games for full ground references. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 312–324. Springer, Heidelberg (2012)
Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3) (2004)
Sakamoto, H., Ikeda, D.: Intractability of decision problems for finite-memory automata. Theor. Comput. Sci. 231(2) (2000)
Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006)
Tan, T.: On pebble automata for data languages with decidable emptiness problem. J. Comput. Syst. Sci. 76(8) (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag GmbH Berlin Heidelberg
About this paper
Cite this paper
Murawski, A.S., Ramsay, S.J., Tzevelekos, N. (2014). Reachability in Pushdown Register Automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44522-8_39
Download citation
DOI: https://doi.org/10.1007/978-3-662-44522-8_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44521-1
Online ISBN: 978-3-662-44522-8
eBook Packages: Computer ScienceComputer Science (R0)