Abstract
In this paper we address the problem of solving parity games over the configuration graphs of bounded phase multi-pushdown systems. A non-elementary decision procedure was proposed for this problem by A. Seth. In this paper, we provide a simple and inductive construction to solve this problem. We also prove a non-elementary lower-bound, answering a question posed by A. Seth.
The authors acknowledge partial support by Indo-French Project AVeCSo, TCS-Fellowship, Indo-Swedish DST-VR Project P-02/2014, Infosys Foundation.
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
Similar content being viewed by others
References
Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. Electr. Notes Theor. Comput. Sci. 68, 1–15 (2002)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1–4 October (1991)
Kupferman, O., Piterman, N., Vardi, M.Y.: An automata-theoretic approach to infinite-state systems. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 202–259. Springer, Heidelberg (2010). doi:10.1007/978-3-642-13754-9_11
Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31980-1_7
Saivasan, P.: Analysis of Automata-theoretic models of Concurrent Recursive Programs. Ph.D. thesis, Chennai Mathematical Institute (2016)
Serre, O.: Note on winning positions on pushdown games with [omega]-regular conditions. Inf. Process. Lett. 85, 285–291 (2003)
Seth, A.: Games on multi-stack pushdown systems. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 395–408. Springer, Heidelberg (2008). doi:10.1007/978-3-540-92687-0_27
Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis. MIT, Cambridge (1974)
Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS. IEEE Computer Society (2007)
Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477–492. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_36
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). doi:10.1007/3-540-61474-5_58
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P. (2017). Parity Games on Bounded Phase Multi-pushdown Systems. In: El Abbadi, A., Garbinato, B. (eds) Networked Systems. NETYS 2017. Lecture Notes in Computer Science(), vol 10299. Springer, Cham. https://doi.org/10.1007/978-3-319-59647-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-59647-1_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-59646-4
Online ISBN: 978-3-319-59647-1
eBook Packages: Computer ScienceComputer Science (R0)