{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T07:40:02Z","timestamp":1748850002289,"version":"3.41.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319325811"},{"type":"electronic","value":"9783319325828"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-32582-8_8","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T10:04:23Z","timestamp":1460023463000},"page":"111-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Certification for $$\\mu $$ \u03bc -Calculus with Winning Strategies"],"prefix":"10.1007","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Neukirchen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,8]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-48092-7_8","volume-title":"Correct System Design","author":"A Biere","year":"1999","unstructured":"Biere, A., Zhu, Y., Clarke, E.: Multiple state and single state tableaux for combining local and global model checking. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 163\u2013179. Springer, Heidelberg (1999)"},{"issue":"1","key":"8_CR2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R Bloem","year":"2006","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in $$n$$ n log $$n$$ n symbolic steps. Formal Methods Syst. Des. 28(1), 37\u201356 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","volume":"3","author":"J Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. Stud. Logic Pract. Reasoning 3, 721\u2013756 (2007)","journal-title":"Stud. Logic Pract. Reasoning"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/B978-044482830-9\/50022-9","volume-title":"Handbook of Process Algebra","author":"J Bradfield","year":"2001","unstructured":"Bradfield, J., Stirling, C.: Modal logics and mu-calculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 293\u2013330. Elsevier, Amsterdam (2001)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-61042-1_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Buhrke","year":"1996","unstructured":"Buhrke, N., Lescow, H., V\u00f6ge, J.: Strategy construction in infinite games with streett and rabin chain winning conditions. In: Margaria, T., Steffen, B. (eds.) TACAS. LNCS, vol. 1055, pp. 207\u2013225. Springer, Heidelberg (1996)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 19\u201329. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of the 32nd Annual ACM\/IEEE Design Automation Conference, pp. 427\u2013432. ACM (1995)","DOI":"10.1145\/217474.217565"},{"issue":"8","key":"8_CR8","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R.: Tableau-based model checking in the propositional mu-calculus. Acta Informatica 27(8), 725\u2013747 (1990)","journal-title":"Acta Informatica"},{"key":"8_CR9","unstructured":"Duret-Lutz, A.: Contributions \u00e0 l\u2019approche automate pour la v\u00e9rification de propri\u00e9t\u00e9s de syst\u00e8mes concurrents. Ph.D. thesis, Universit\u00e9 Pierre et Marie Curie (Paris 6) July 2007. https:\/\/www.lrde.epita.fr\/~adl\/th.html"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-04761-9_17","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2009","unstructured":"Duret-Lutz, A., Poitrenaud, D., Couvreur, J.-M.: On-the-fly emptiness check of transition-based streett automata. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 213\u2013227. Springer, Heidelberg (2009)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Computer Aided Verification","author":"E Emerson","year":"1993","unstructured":"Emerson, E., Jutla, C., Sistla, A.: On model-checking for fragments of $$\\mu $$ \u03bc -calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385\u2013396. Springer, Heidelberg (1993)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS 1991), pp. 368\u2013377. IEEE (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1017\/CBO9780511973468.005","volume-title":"Lectures in Game Theory for Computer Scientists","author":"E Gr\u00e4del","year":"2011","unstructured":"Gr\u00e4del, E.: Back and forth between logic and games. In: Apt, K., Gr\u00e4del, E. (eds.) Lectures in Game Theory for Computer Scientists, pp. 99\u2013138. Cambridge University Press, Cambridge (2011)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-36577-X_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160\u2013175. Springer, Heidelberg (2003)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-61422-2_117","volume-title":"Algorithm Theory - SWAT \u201996","author":"MR Henzinger","year":"1996","unstructured":"Henzinger, M.R., Telle, J.A.: Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: Karlsson, R., Lingas, A. (eds.) SWAT 1996. LNCS, vol. 1097, pp. 16\u201327. Springer, Heidelberg (1996)"},{"key":"8_CR16","unstructured":"Hofmann, M., Rue\u00df, H.: Certification for $$\\mu $$ \u03bc -calculus with winning strategies. ArXiv e-prints, January 2014"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1017\/CBO9780511973468.004","volume-title":"Lectures in Game Theory for Computer Scientists","author":"M Jurdzi\u0144ski","year":"2011","unstructured":"Jurdzi\u0144ski, M.: Algorithms for solving parity games. In: Apt, K., Gr\u00e4del, E. (eds.) Lectures in Game Theory for Computer Scientists, pp. 74\u201398. Cambridge University Press, Cambridge (2011)"},{"key":"8_CR18","unstructured":"Kick, A.: Generation of counterexamples for the $$\\mu $$ \u03bc -calculus. Technical report ira-tr-1995-37, Universit\u00e4t Karlsruhe, Germany (1995)"},{"issue":"2","key":"8_CR19","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_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"8_CR22","unstructured":"Neukirchen, C.: Computation of winning strategies for $$\\mu $$ \u03bc -calculus by fixpoint iteration. Master\u2019s thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, November 2014"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"DA Peled","year":"2001","unstructured":"Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292\u2013304. Springer, Heidelberg (2001)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-45221-5_44","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E Renault","year":"2013","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized B\u00fcchi automata. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 668\u2013682. Springer, Heidelberg (2013)"},{"key":"8_CR26","unstructured":"Seidl, H.: Fast and Simple Nested Fixpoints. Universit\u00e4t Trier, Mathematik\/Informatik, Forschungsbericht 96-05 (1996)"},{"key":"8_CR27","unstructured":"Shankar, N., Sorea, M.: Counterexample-driven model checking (revisited version). Technical report SRI-CSL-03-04, SRI International (2003)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-16310-4_1","volume-title":"Rewriting Logic and Its Applications","author":"N Shankar","year":"2010","unstructured":"Shankar, N.: Rewriting, inference, and proof. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 1\u201314. Springer, Heidelberg (2010)"},{"key":"8_CR29","unstructured":"Sorea, M.: Dubious witnesses and spurious counterexamples. UK Model Checking Days, York (2005). http:\/\/www.cs.man.ac.uk\/~msorea\/talks\/york.pdf"},{"key":"8_CR30","unstructured":"Sorea, M.: Verification of real-time systems through lazy approximations. Ph.D. thesis, University of Ulm, Germany (2004)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-50939-9_144","volume-title":"TAPSOFT 1989","author":"C Stirling","year":"1989","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. In: D\u00edaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 351, pp. 369\u2013383. Springer, Heidelberg (1989)"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-13345-3_43","volume-title":"Automata, Languages and Programming","author":"RS Streett","year":"1984","unstructured":"Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) Automata, Languages and Programming. LNCS, vol. 172, pp. 465\u2013472. Springer, Heidelberg (1984)"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Computer Aided Verification","author":"L Tan","year":"2002","unstructured":"Tan, L., Cleaveland, W.R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455\u2013470. Springer, Heidelberg (2002)"},{"key":"8_CR34","unstructured":"Vardi, M., Wilke, T.: Automata: from logics to algorithms. In: WAL, pp. 645\u2013753 (2007)"},{"issue":"1","key":"8_CR35","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(91)90043-2","volume":"83","author":"G Winskel","year":"1991","unstructured":"Winskel, G.: A note on model checking the modal $$\\nu $$ \u03bd -calculus. Theor. Comput. Sci. 83(1), 157\u2013167 (1991)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T07:05:31Z","timestamp":1748847931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}