{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:19:23Z","timestamp":1740097163072,"version":"3.37.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319278094"},{"type":"electronic","value":"9783319278100"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-27810-0_8","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T02:38:33Z","timestamp":1450924713000},"page":"159-177","source":"Crossref","is-referenced-by-count":3,"title":["Static Analysis of Parity Games: Alternating Reachability Under Parity"],"prefix":"10.1007","author":[{"given":"Michael","family":"Huth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim Huan-Pu","family":"Kuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"8_CR1","unstructured":"Chatterjee, K.: Linear time algorithm for weak parity games. CoRR abs\/0805.1391 (2008)"},{"issue":"5","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, January 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: past, present and future. In: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, 14\u201318 July 2014, p. 2 (2014)","DOI":"10.1145\/2603088.2603165"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theor. Comput. Sci. 126(1), 77\u201396 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-540-87531-4_26","volume-title":"Computer Science Logic","author":"A Dawar","year":"2008","unstructured":"Dawar, A., Gr\u00e4del, E.: The descriptive complexity of parity games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 354\u2013368. Springer, Heidelberg (2008)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"8_CR8","unstructured":"Emerson, E., Jutla, C.: Tree automata, \n                    \n                      \n                    \n                    $$\\mu $$\n                  -calculus and determinacy. In: Proceedings 32nd IEEE Symposium on Foundations of Computer Science, pp. 368\u2013377 (1991)"},{"issue":"3","key":"8_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Computer Aided Verification","author":"E. A. Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \n                    \n                      \n                    \n                    $$\\rm \\mu $$\n                  -calculus. In: Proceedings of 5th International Conference on Computer Aided Verification, CAV 1993, Elounda, 28 June - 1 July, 1993, pp. 385\u2013396 (1993)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Filipiuk, P., Nielson, F., Nielson, H.R.: Layered fixed point logic. CoRR abs\/1204.2768 (2012)","DOI":"10.1145\/2370776.2370784"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-04761-9_15","volume-title":"Automated Technology for Verification and Analysis","author":"O Friedmann","year":"2009","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182\u2013196. Springer, Heidelberg (2009)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-37075-5_3","volume-title":"Foundations of Software Science and Computation Structures","author":"M Huth","year":"2013","unstructured":"Huth, M., Kuo, J.H.-P., Piterman, N.: Fatal attractors in parity games. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 34\u201349. Springer, Heidelberg (2013)"},{"key":"8_CR14","unstructured":"Huth, M., Kuo, J.H., Piterman, N.: Fatal attractors in parity games: building blocks for partial solvers. CoRR abs\/1405.0386 (2014)"},{"key":"8_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science - Modelling and Reasoning About Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, New York (2004)","edition":"2"},{"key":"8_CR16","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\n                    \n                      \n                    \n                    $${}\\cap {}$$\n                  co-UP. Inf. Process. Lett. 68, 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"8_CR18","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-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983). \n                    http:\/\/dx.doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"DA Martin","year":"1975","unstructured":"Martin, D.A.: Borel determinacy. Ann. Math. 102(2), 363\u2013371 (1975)","journal-title":"Ann. Math."},{"key":"8_CR21","unstructured":"Mostowski, A.W.: Games with forbidden positions. Technical Report 78, University of Gda\u0144sk (1991)"},{"key":"8_CR22","unstructured":"Nielson, F., Nielson, H.R.: Model checking is static analysis of modal logic. In: Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, 20\u201328 March, 2010. Proceedings, pp. 191\u2013205 (2010)"},{"key":"8_CR23","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis (2. corr. print). Springer, Heidelberg (2005)"},{"key":"8_CR24","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: International Symposium on Programming, 5th Colloquium, Torino, Italy, 6\u20138 April, 1982, Proceedings, pp. 337\u2013351 (1982)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"DA Schmidt","year":"1998","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"8_CR26","first-page":"346","volume-title":"Lecture Notes in Computer Science","author":"Bernhard Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Theoretical Aspects of Computer Software, International Conference TACS 1991, Sendai, Japan, 24\u201327 September, 1991, Proceedings, pp. 346\u2013365 (1991)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Lokal model checking games. In: CONCUR 1995: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21\u201324, 1995, Proceedings, pp. 1\u201311 (1995)","DOI":"10.1007\/3-540-60218-6_1"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-30729-4_8","volume-title":"Integrated Formal Methods","author":"F Zhang","year":"2012","unstructured":"Zhang, F., Nielson, F., Nielson, H.R.: Model checking as static analysis: revisited. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 99\u2013112. Springer, Heidelberg (2012)"},{"issue":"1\u20132","key":"8_CR29","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":["Lecture Notes in Computer Science","Semantics, Logics, and Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27810-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:00:35Z","timestamp":1559350835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27810-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783319278094","9783319278100"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27810-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}