Recursive algorithm for parity games requires exponential time
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 4, pp. 449-457.

This paper presents a new lower bound for the recursive algorithm for solving parity games which is induced by the constructive proof of memoryless determinacy by Zielonka. We outline a family of games of linear size on which the algorithm requires exponential time.

DOI : https://doi.org/10.1051/ita/2011124
Classification : 05C57
Mots clés : parity games, recursive algorithm, lower bound, μcalculus, model checking
@article{ITA_2011__45_4_449_0,
author = {Friedmann, Oliver},
title = {Recursive algorithm for parity games requires exponential time},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {449--457},
publisher = {EDP-Sciences},
volume = {45},
number = {4},
year = {2011},
doi = {10.1051/ita/2011124},
zbl = {1232.91064},
mrnumber = {2876116},
language = {en},
url = {http://www.numdam.org/articles/10.1051/ita/2011124/}
}
TY  - JOUR
AU  - Friedmann, Oliver
TI  - Recursive algorithm for parity games requires exponential time
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2011
DA  - 2011///
SP  - 449
EP  - 457
VL  - 45
IS  - 4
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2011124/
UR  - https://zbmath.org/?q=an%3A1232.91064
UR  - https://www.ams.org/mathscinet-getitem?mr=2876116
UR  - https://doi.org/10.1051/ita/2011124
DO  - 10.1051/ita/2011124
LA  - en
ID  - ITA_2011__45_4_449_0
ER  - 
Friedmann, Oliver. Recursive algorithm for parity games requires exponential time. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 4, pp. 449-457. doi : 10.1051/ita/2011124. http://www.numdam.org/articles/10.1051/ita/2011124/

[1] E.A. Emerson and C.S. Jutla, Tree automata, μ-calculus and determinacy, in Proc. 32nd Symp. on Foundations of Computer Science. San Juan, Puerto Rico, IEEE (1991) 368-377.

[2] E.A. Emerson, C.S. Jutla and A.P. Sistla, On model-checking for fragments of μ-calculus, in Proc. 5th Conf. on Computer Aided Verification, CAV'93. Lect. Notes Comput. Sci. 697 (1993) 385-396. | MR 1254452

[3] O. Friedmann, An exponential lower bound for the parity game strategy improvement algorithm as we know it, in Proc. of LICS (2009) 145-156. | MR 2932379

[4] O. Friedmann and M. Lange, Solving parity games in practice, in Proc. of ATVA (2009) 182-196. | Zbl 1258.68077

[5] E. Grädel, W. Thomas and Th. Wilke Eds., Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500 (2002). | Zbl 1011.00037

[6] M. Jurdzinski, Deciding the winner in parity games is in up ∩ co − up. Inf. Process. Lett. 68 (1998) 119-124. | MR 1657581

[7] M. Jurdziński, Small progress measures for solving parity games, in Proc. 17th Ann. Symp. on Theoretical Aspects of Computer Science, STACS'00, edited by H. Reichel and S. Tison. Lect. Notes Comput. Sci. 1770 (2000) 290-301. | MR 1781740 | Zbl 0962.68111

[8] M. Jurdziński, M. Paterson and U. Zwick, A deterministic subexponential algorithm for solving parity games, in Proc. 17th Ann. ACM-SIAM Symp. on Discrete Algorithm, SODA'06. ACM (2006) 117-123. | MR 2368806 | Zbl 1192.91013

[9] S. Schewe, Solving parity games in big steps, in Proc. FST TCS. Springer-Verlag (2007). | MR 2480222 | Zbl 1135.68480

[10] S. Schewe, An optimal strategy improvement algorithm for solving parity and payoff games, in 17th Annual Conference on Computer Science Logic (CSL) (2008). | MR 2540256 | Zbl 1156.68478

[11] P. Stevens and C. Stirling, Practical model-checking using games, in Proc. 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'98, edited by B. Steffen. Lect. Notes Comput. Sci. 1384 (1998) 85-101.

[12] C. Stirling, Local model checking games, in Proc. 6th Conf. on Concurrency Theory, CONCUR'95. Lect. Notes Comput. Sci. 962 (1995) 1-11.

[13] J. Vöge and M. Jurdziński, A discrete strategy improvement algorithm for solving parity games, in Proc. 12th Int. Conf. on Computer Aided Verification, CAV'00. Lect. Notes Comput. Sci. 1855 (2000) 202-215. | Zbl 0974.68527

[14] W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci. 200 (1998) 135-183. | MR 1625527 | Zbl 0915.68120

Cité par Sources :