{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:44:42Z","timestamp":1725525882096},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642004308"},{"type":"electronic","value":"9783642004315"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00431-5_2","type":"book-chapter","created":{"date-parts":[[2009,2,24]],"date-time":"2009-02-24T06:14:35Z","timestamp":1235456075000},"page":"15-33","source":"Crossref","is-referenced-by-count":7,"title":["Solving \u03bc-Calculus Parity Games by Symbolic Planning"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bakera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Kissmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens D.","family":"Renner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Bakera, M., Margaria, T., Renner, C.D., Steffen, B.: Game-based model checking for reliable autonomy in space. Journal of the American Institute of Aeronautics and Astronautics (AIAA) (to appear)","DOI":"10.2514\/1.32013"},{"key":"2_CR2","unstructured":"Bakera, M., Margaria, T., Renner, C.D., Steffen, B.: Verification, diagnosis and adaptation: Tool supported enhancement of the model-driven verification process. In: Revue des Nouvelles Technologies de Information (RNTI-SM-1), pp. 85\u201398 (to appear) ISBN 2854288148"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/3-540-63166-6_50","volume-title":"Computer Aided Verification","author":"A. Biere","year":"1997","unstructured":"Biere, A.: \u03bccke \u2013 efficient \u03bc-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 468\u2013471. Springer, Heidelberg (1997)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. Tools and Algorithms for the Construction and Analysis of Systems (1999)","DOI":"10.21236\/ADA360973"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-36494-3_58","volume-title":"STACS 2003","author":"H. Bj\u00f6rklund","year":"2003","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.G.: A discrete subexponential algorithm for parity games. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 663\u2013674. Springer, Heidelberg (2003)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic manipulation of Boolean functions using a graphical representation. In: ACM\/IEEE Design Automation Conference, pp. 688\u2013694 (1985)","DOI":"10.1109\/DAC.1985.1586017"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1007\/978-3-540-24749-4_46","volume-title":"STACS 2004","author":"D. Bustan","year":"2004","unstructured":"Bustan, D., Kupferman, O., Vardi, M.Y.: A measured collapse of the modal \u03bc-calculus alternation hierarchy. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol.\u00a02996, pp. 522\u2013533. Springer, Heidelberg (2004)"},{"key":"2_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"2_CR9","first-page":"410","volume":"663","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal \u03bc-calculus. Theoretical Computer Science\u00a0663, 410\u2013422 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design\u00a02(2), 121\u2013147 (1993)","journal-title":"Formal Methods in System Design"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-73368-3_13","volume-title":"Computer Aided Verification","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 108\u2013120. Springer, Heidelberg (2007)"},{"key":"2_CR12","unstructured":"Edelkamp, S.: Symbolic exploration in two-player games: Preliminary results. In: AIPS-Workshop on Model Checking, pp. 40\u201348 (2002)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/10720246_11","volume-title":"Recent Advances in AI Planning","author":"S. Edelkamp","year":"2000","unstructured":"Edelkamp, S., Helmert, M.: Exhibiting knowledge in planning problems to minimize state encoding length. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 135\u2013147. Springer, Heidelberg (2000)"},{"key":"2_CR14","unstructured":"Edelkamp, S., Kissmann, P.: Symbolic exploration for general game playing in PDDL. In: ICAPS-Workshop on Planning in Games (2007)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-540-85845-4_23","volume-title":"KI 2008: Advances in Artificial Intelligence","author":"S. Edelkamp","year":"2008","unstructured":"Edelkamp, S., Kissmann, P.: Symbolic classification of general two-player games. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS, vol.\u00a05243, pp. 185\u2013192. Springer, Heidelberg (2008)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata \u03bc-calculus and determinacy. In: Foundations of Computer Science, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"2_CR17","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Symposium on Logic in Computer Science, pp. 267\u2013278 (1986)"},{"key":"2_CR18","unstructured":"Genesereth, M.R.: Knowledge interchange format. In: Second International Conference on Principles of Knowledge Representation and Reasoning, pp. 238\u2013249 (1991)"},{"key":"2_CR19","unstructured":"Helmert, M.: A planning heuristic based on causal graph analysis. In: International Conference on Automated Planning and Scheduling, pp. 161\u2013170 (2004)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"Automata, Languages and Programming","author":"M. Hennessy","year":"1980","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 299\u2013309. Springer, Heidelberg (1980)"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"J\u00f8rges, S., Kubczak, C., Pageau, F., Margaria, T.: Model driven design of reliable robot control programs using the jabc. In: 4th IEEE International Workshop on Engineering of Autonomic and Autonomous Systems (EASe), March 2007, pp. 137\u2013148 (2007)","DOI":"10.1109\/EASE.2007.17"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzinski","year":"1998","unstructured":"Jurdzinski, M.: Deciding the winner in parity games is UP\u2229co-UP. Information Processing Letters\u00a068(3), 119\u2013124 (1998)","journal-title":"Information Processing Letters"},{"key":"2_CR23","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. Jurdzinski","year":"2000","unstructured":"Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: SODA, pp. 117\u2013123 (2006)","DOI":"10.1145\/1109557.1109571"},{"key":"2_CR25","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: Planning propositional logic, and stochastic search. In: European Conference on Artificial Intelligence, pp. 1194\u20131201 (1996)"},{"key":"2_CR26","unstructured":"Love, N.C., Hinrichs, T.L., Genesereth, M.R.: General game playing: Game description language specification. Technical Report LG-2006-01, Stanford Logic Group (April 2006)"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Nam, W., Alur, R.: Symbolic computational techniques for solving games. Electronic Notes in Theoretical Computer Science\u00a089(4) (2004)","DOI":"10.1016\/S1571-0661(05)82544-7"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0168-0072(93)90036-D","volume":"65","author":"R. McNaughton","year":"1993","unstructured":"McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic\u00a065, 129\u2013284 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"key":"2_CR29","unstructured":"Schaeffer, J., Bj\u00f6rnsson, Y., Burch, N., Kishimoto, A., M\u00fcller, M., Lake, R., Lu, P., Sutphen, S.: Solving checkers. In: International Joint Conference on Artificial Intelligence, pp. 292\u2013297 (2005)"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Schewe, S.: Solving parity games in big steps. In: CAV, pp. 449\u2013460 (2007)","DOI":"10.1007\/978-3-540-77050-3_37"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Conference Record of POPL 1998: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, Janary 19\u201321, 1998, pp. 38\u201348 (1998)","DOI":"10.1145\/268946.268950"},{"issue":"2-3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. STTT\u00a05(2-3), 185\u2013204 (2004)","journal-title":"STTT"},{"issue":"6","key":"2_CR33","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0020-0190(96)00130-5","volume":"59","author":"H. Seidl","year":"1996","unstructured":"Seidl, H.: Fast and simple nested fixpoints. Information Processing Letters\u00a059(6), 119\u2013124 (1996)","journal-title":"Information Processing Letters"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B. Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 346\u2013365. Springer, Heidelberg (1991)"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995 Concurrency Theory","author":"B. Steffen","year":"1995","unstructured":"Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 72\u201387. Springer, Heidelberg (1995)"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60218-6_1","volume-title":"CONCUR \u201995 Concurrency Theory","author":"C. Stirling","year":"1995","unstructured":"Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 1\u201311. Springer, Heidelberg (1995)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-59042-0_57","volume-title":"STACS 95","author":"W. Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol.\u00a0900, pp. 1\u201313. Springer, Heidelberg (1995)"},{"key":"2_CR38","unstructured":"van de Pol, J., Weber, M.: A multi-core solver for parity games. In: PDMC 2008 (to appear, 2008)"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/10722167_18","volume-title":"Computer Aided Verification","author":"J. V\u00f6ge","year":"2000","unstructured":"V\u00f6ge, J., Jurdzinski, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 202\u2013215. Springer, Heidelberg (2000)"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/BFb0031395","volume-title":"Automata Implementation","author":"J. V\u00f6ge","year":"1998","unstructured":"V\u00f6ge, J., Ulbrand, S., Matz, O., Buhrke, N.: The automata theory package omega. In: Wood, D., Yu, S. (eds.) WIA 1997. LNCS, vol.\u00a01436, pp. 228\u2013231. Springer, Heidelberg (1998)"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/3-540-45089-0_3","volume-title":"Implementation and Application of Automata","author":"N. Wallmeier","year":"2003","unstructured":"Wallmeier, N., H\u00fctten, P., Thomas, W.: Symbolic synthesis of finite-state controllers for request-response specifications. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 11\u201322. Springer, Heidelberg (2003)"},{"key":"2_CR42","unstructured":"Yoo, H.: Fehlerdiagnose beim Model-Checking durch animierte Strategiesynthese. PhD thesis, Universit\u00e4t Dortmund (2007)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-24730-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Yoo","year":"2004","unstructured":"Yoo, H., M\u00fcller-Olm, M.: MetaGame: An animation tool for model-checking games. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 163\u2013167. Springer, Heidelberg (2004)"},{"key":"2_CR44","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 finite coloured graphs with applications to automata on infinite trees. Theoretical Computer Science\u00a0200, 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00431-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T06:33:35Z","timestamp":1558161215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00431-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642004308","9783642004315"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00431-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}