{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T03:40:11Z","timestamp":1721014811168},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T00:00:00Z","timestamp":1551052800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10009-019-00509-3","type":"journal-article","created":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T07:35:15Z","timestamp":1551080115000},"page":"325-349","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space"],"prefix":"10.1007","volume":"21","author":[{"given":"John","family":"Fearnley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjay","family":"Jain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"de Keijzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Stephan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Wojtczak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,25]]},"reference":[{"issue":"5","key":"509_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"509_CR2","volume-title":"Information Theory","author":"RB Ash","year":"1990","unstructured":"Ash, R.B.: Information Theory. Dover Publications Inc., New York (1990)"},{"key":"509_CR3","doi-asserted-by":"crossref","unstructured":"Berwanger, D., Dawar, A., Hunter, P., Kreutzer, S.: Dag-width and parity games. In: Proceedings of STACS, pp. 524\u2013436. Springer, Berlin (2006)","DOI":"10.1007\/11672142_43"},{"issue":"2","key":"509_CR4","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.dam.2006.04.029","volume":"155","author":"H Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Appl. Math. 155(2), 210\u2013229 (2007). https:\/\/doi.org\/10.1016\/j.dam.2006.04.029","journal-title":"Discrete Appl. Math."},{"issue":"1\u20132","key":"509_CR5","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/S0304-3975(96)00228-9","volume":"178","author":"A Browne","year":"1997","unstructured":"Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. TCS 178(1\u20132), 237\u2013255 (1997)","journal-title":"TCS"},{"key":"509_CR6","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, pp. 252\u2013263. ACM (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"509_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M., Loitzenbauer, V.: Improved algorithms for one-pair and k-pair streett objectives. In: Proceedings of LICS, pp. 269\u2013280. IEEE Computer Society (2015)","DOI":"10.1109\/LICS.2015.34"},{"key":"509_CR8","unstructured":"de\u00a0Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: Proceedings of LICS, pp. 279\u2013290 (2001)"},{"key":"509_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of $$\\mu $$ \u03bc -calculus. In: Proceedings of CAV, pp. 385\u2013396 (1993)","DOI":"10.1007\/3-540-56922-7_32"},{"key":"509_CR10","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, $$\\mu $$ \u03bc -calculus and determinacy. In: Proceedings of FOCS, pp. 368\u2013377. IEEE Computer Society Press (1991)"},{"key":"509_CR11","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional $$\\mu $$ \u03bc -calculus. In: Proceedings of LICS, pp. 267\u2013278. IEEE Computer Society Press (1986)"},{"key":"509_CR12","unstructured":"Fearnley, J., Jain, S., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10\u201314, 2017, pp. 112\u2013121. ACM (2017)"},{"key":"509_CR13","doi-asserted-by":"crossref","unstructured":"Fearnley, J.: Non-oblivious strategy improvement. In: Proceedings of LPAR, pp. 212\u2013230 (2010)","DOI":"10.1007\/978-3-642-17511-4_13"},{"key":"509_CR14","unstructured":"Friedmann, O., Lange, M.: PGSolver version 4.0 (2017). https:\/\/github.com\/tcsprojects\/pgsolver"},{"key":"509_CR15","doi-asserted-by":"crossref","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Proceedings of ATVA, pp. 182\u2013196 (2009)","DOI":"10.1007\/978-3-642-04761-9_15"},{"key":"509_CR16","unstructured":"Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. University of Munich (2014). http:\/\/www.win.tue.nl\/~timw\/downloads\/amc2014\/pgsolver.pdf"},{"key":"509_CR17","doi-asserted-by":"crossref","unstructured":"Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. LMCS 7(3) (2011)","DOI":"10.2168\/LMCS-7(3:23)2011"},{"issue":"4","key":"509_CR18","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1051\/ita\/2011124","volume":"45","author":"O Friedmann","year":"2011","unstructured":"Friedmann, O.: Recursive algorithm for parity games requires exponential time. RAIRO-Theor. Inf. Appl. 45(4), 449\u2013457 (2011)","journal-title":"RAIRO-Theor. Inf. Appl."},{"key":"509_CR19","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Proceedings of CAV, LNCS, vol. 9780, pp. 291\u2013311 (2016)","DOI":"10.1007\/978-3-319-41540-6_16"},{"key":"509_CR20","unstructured":"Jurdzi\u0144ski, M., Lazi\u0107, R.: Succinct progress measures for solving parity games. In: Proceedings of LICS 2017, p. (to appear) (2017). arXiv:1702.05051"},{"key":"509_CR21","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: Proceedings of SODA, pp. 117\u2013123. ACM\/SIAM (2006)","DOI":"10.1145\/1109557.1109571"},{"key":"509_CR22","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Proceedings of STACS, pp. 290\u2013301. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46541-3_24"},{"issue":"3","key":"509_CR23","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M Jurdzi\u0144ski","year":"1998","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in UP $$\\cap $$ \u2229 co-UP. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"key":"509_CR24","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ \u03bc -calculus. TCS 27, 333\u2013354 (1983)","journal-title":"TCS"},{"key":"509_CR25","unstructured":"Lange, M.: Solving parity games by a reduction to SAT. In: Proceedings of International Workshop on Games in Design and Verification (2005)"},{"key":"509_CR26","unstructured":"Lehtinen, K.: A modal $$\\mu $$ \u03bc perspective on solving parity games in quasi-polynomial time. To appear in the proceedings of LiCS\u201918"},{"issue":"1","key":"509_CR27","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.1995.1035","volume":"117","author":"W Ludwig","year":"1995","unstructured":"Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Inf. Comput. 117(1), 151\u2013155 (1995)","journal-title":"Inf. Comput."},{"issue":"2","key":"509_CR28","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0168-0072(93)90036-D","volume":"65","author":"R McNaughton","year":"1993","unstructured":"McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Log. 65(2), 149\u2013184 (1993)","journal-title":"Ann. Pure Appl. Log."},{"key":"509_CR29","doi-asserted-by":"crossref","unstructured":"Obdr\u017e\u00e1lek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Proceedings of CAV, pp. 80\u201392. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_7"},{"key":"509_CR30","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Proceedings of LICS, pp. 255\u2013264. IEEE Computer Society (2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"509_CR31","unstructured":"Puri, A.: Theory of hybrid systems and discrete event systems. Ph.D. thesis, Computer Science Department, University of California, Berkeley (1995)"},{"key":"509_CR32","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Proceedings of LOPSTR, pp. 127\u2013142. Springer, Berlin (2006)","DOI":"10.1007\/978-3-540-71410-1_10"},{"key":"509_CR33","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: The alternating-time $$\\mu $$ \u03bc -calculus and automata over concurrent game structures. In: Proceedings of CSL, pp. 591\u2013605. Springer, Berlin (2006)","DOI":"10.1007\/11874683_39"},{"key":"509_CR34","doi-asserted-by":"crossref","unstructured":"Schewe, S., Trivedi, A., Varghese, T.: Symmetric strategy improvement. In: Proceedings of ICALP, LNCS, vol. 9135, pp. 388\u2013400 (2015)","DOI":"10.1007\/978-3-662-47666-6_31"},{"key":"509_CR35","doi-asserted-by":"crossref","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Proceedings of CSL 2008, pp. 368\u2013383. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-87531-4_27"},{"key":"509_CR36","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/j.jcss.2016.10.002","volume":"84","author":"S Schewe","year":"2017","unstructured":"Schewe, S.: Solving parity games in big steps. J. Comput. Syst. Sci. 84, 243\u2013262 (2017)","journal-title":"J. Comput. Syst. Sci."},{"key":"509_CR37","unstructured":"Totzke, P.: Implementation of the succinct progress measures algorithm from [22] (2017). https:\/\/github.com\/pazz\/pgsolver\/tree\/sspm"},{"key":"509_CR38","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Proceedings of ICALP, pp. 628\u2013641. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055090"},{"key":"509_CR39","doi-asserted-by":"crossref","unstructured":"V\u00f6ge, J., Jurdzi\u0144ski, M.: A discrete strategy improvement algorithm for solving parity games. In: Proceedings of the CAV, pp. 202\u2013215. Springer, Berlin (2000)","DOI":"10.1007\/10722167_18"},{"issue":"2","key":"509_CR40","doi-asserted-by":"crossref","first-page":"359","DOI":"10.36045\/bbms\/1102714178","volume":"8","author":"T Wilke","year":"2001","unstructured":"Wilke, T.: Alternating tree automata, parity games, and modal $$\\mu $$ \u03bc -calculus. Bull. Soc. Math. Belg. 8(2), 359 (2001)","journal-title":"Bull. Soc. Math. Belg."},{"issue":"1\u20132","key":"509_CR41","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00509-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00509-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00509-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T02:39:37Z","timestamp":1721011177000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00509-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,25]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["509"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00509-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,25]]},"assertion":[{"value":"25 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}