Recursive algorithm for parity games requires exponential time

Oliver Friedmann

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2011)

  • Volume: 45, Issue: 4, page 449-457
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Friedmann, Oliver. "Recursive algorithm for parity games requires exponential time." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 45.4 (2011): 449-457. <http://eudml.org/doc/273062>.

@article{Friedmann2011,
abstract = {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.},
author = {Friedmann, Oliver},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {parity games; recursive algorithm; lower bound; μcalculus; model checking; -calculus},
language = {eng},
number = {4},
pages = {449-457},
publisher = {EDP-Sciences},
title = {Recursive algorithm for parity games requires exponential time},
url = {http://eudml.org/doc/273062},
volume = {45},
year = {2011},
}

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
PB - EDP-Sciences
VL - 45
IS - 4
SP - 449
EP - 457
AB - 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.
LA - eng
KW - parity games; recursive algorithm; lower bound; μcalculus; model checking; -calculus
UR - http://eudml.org/doc/273062
ER -

References

top
  1. [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. [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. MR1254452
  3. [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. MR2932379
  4. [4] O. Friedmann and M. Lange, Solving parity games in practice, in Proc. of ATVA (2009) 182–196. Zbl1258.68077
  5. [5] E. Grädel, W. Thomas and Th. Wilke Eds., Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500 (2002). Zbl1011.00037
  6. [6] M. Jurdzinski, Deciding the winner in parity games is in up ∩ co − up. Inf. Process. Lett. 68 (1998) 119–124. Zbl06590783MR1657581
  7. [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. Zbl0962.68111MR1781740
  8. [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. Zbl1192.91013MR2368806
  9. [9] S. Schewe, Solving parity games in big steps, in Proc. FST TCS. Springer-Verlag (2007). Zbl1135.68480MR2480222
  10. [10] S. Schewe, An optimal strategy improvement algorithm for solving parity and payoff games, in 17th Annual Conference on Computer Science Logic (CSL) (2008). Zbl1156.68478MR2540256
  11. [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. [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. [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. Zbl0974.68527
  14. [14] W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci.200 (1998) 135–183. Zbl0915.68120MR1625527

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.