Abstract
Bounded phase multi-stack pushdown automata have been studied recently. In this paper we show that parity games over bounded phase multi-stack pushdown systems are effectively solvable and winning strategy in these games can be effectively synthesized. We show some applications of our result, including a new proof of a known result that emptiness problem for bounded phase multi-stack automata is decidable.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Madhusudan, P., Parlato, G., La Torre, S.: A Robust Class of Context-Sensitive Languages. In: 22nd IEEE Symp. on Logic in Computer Science (LICS) Wroclaw, Poland (2007)
Madhusudan, P., Parlato, G., La Torre, S.: An Infinite Automaton Characterization of Double Exponential Time. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 33–48. Springer, Heidelberg (2008)
Madhusudan, P., Parlato, G., La Torre, S.: Context-Bounded Analysis of Concurrent Queue Systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008)
Lal, A., Reps, T.: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 37–51. Springer, Heidelberg (2008)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of the 11th International Symposium on Tools and Algorithms for the Construction and Analysis of Systems (2005)
Kahlon, V., Ivancic, F., Gupta, A.: Reasoning About Threads Communicating via Locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005)
Serre, O.: Note on Winning Positions on Pushdown Games with Omega-Regular Conditions. Information Processing Letters 85(6), 285–291 (2003)
Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. In: Proc. INFINITY. ENTCS, vol. 68(6) (2002)
Walukiewicz, I.: Pushdown processes: games and model checking. Information and computation 164, 234–263 (2001)
Jurdziński, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Proc. Concur, pp. 135–150 (1997)
Thomas, W.: Languages, automata and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. III, pp. 389–455. Springer, New York (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seth, A. (2008). Games on Multi-stack Pushdown Systems. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2009. Lecture Notes in Computer Science, vol 5407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92687-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-92687-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92686-3
Online ISBN: 978-3-540-92687-0
eBook Packages: Computer ScienceComputer Science (R0)