{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:14:42Z","timestamp":1761610482494,"version":"build-2065373602"},"reference-count":25,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3862,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003]]},"DOI":"10.1016\/s1571-0661(05)82544-7","type":"journal-article","created":{"date-parts":[[2005,5,19]],"date-time":"2005-05-19T09:46:30Z","timestamp":1116495990000},"page":"578-592","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":10,"title":["Symbolic Computational Techniques for Solving Games"],"prefix":"10.1016","volume":"89","author":[{"given":"P.","family":"Madhusudan","sequence":"first","affiliation":[]},{"given":"Wonhong","family":"Nam","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)82544-7_BIB1","doi-asserted-by":"crossref","unstructured":"R. Alur, L. de Alfaro, T. Henzinger, and F. Mang. Automating modular verification. In Proceedings of the Tenth International Conference on Concurrency Theory, volume 1664 in LNCS, Springer, pp. 82\u201397, 1999.","DOI":"10.1007\/3-540-48320-9_8"},{"issue":"5","key":"10.1016\/S1571-0661(05)82544-7_BIB2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB3","series-title":"Proceedings of the 10th International Conference on Computer-Aided Verification, volume 1427 of LNCS","first-page":"521","article-title":"Mocha: Modularity in model checking","author":"Alur","year":"1998"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB4","unstructured":"A. Arnold and D. Niwinski. Rudiments of \u03bc-calculus. Studies in Logic and the Foundations of Mathematics 146. 2001."},{"key":"10.1016\/S1571-0661(05)82544-7_BIB5","unstructured":"P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, and P. Traverso. MBP: a Model Based Planner. In Proceedings of IJCAI-2001 workshop on Planning under Uncertainty and Incomplete Information, 2001."},{"key":"10.1016\/S1571-0661(05)82544-7_BIB6","series-title":"Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u203299), volume 1579 in LNCS","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"Biere","year":"1999"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB7","series-title":"Proceedings of the 9th International Conference on Computer-Aided Verification, volume 1254 of LNCS","first-page":"468","article-title":"\u03bccke - Efficient \u03bc-calculus model checking","author":"Biere","year":"1997"},{"issue":"8","key":"10.1016\/S1571-0661(05)82544-7_BIB8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB9","series-title":"Proceedings of the 14th International Conference on Computer-Aided Verification, volume 2404 of LNCS","first-page":"428","article-title":"Interface compatibility checking for software modules","author":"Chakrabarti","year":"2002"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB10","series-title":"Proc. of the International Congress of Mathematicians, 1962","first-page":"23","article-title":"Logic, arithmetics, and automata","author":"Church","year":"1963"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB11","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","article-title":"QUBE: A system for deciding quantified boolean formulas satisfiability","author":"Giunchiglia","year":"2001","journal-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u203201)"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB12","doi-asserted-by":"crossref","unstructured":"E. Goldberg and Y. Novikov. BerkMin: A fast and robust SAT solver. In Proc. of Design Automation and Test in Europe (DATE\u203202), pages 142\u2013149, 2002.","DOI":"10.1109\/DATE.2002.998262"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB13","doi-asserted-by":"crossref","unstructured":"A. Gupta, M. Ganai, C. Wang, Z. Yang, and P.N. Ashar. Learning from BDDs in SAT-based bounded model checking. In Proceedings of the 40th Design Automation Conference (DAC\u203203), 2003.","DOI":"10.1145\/776038.776040"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB14","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1613\/jair.649","article-title":"OBDD-based Universal planning for synchronized agents in non-deterministic domains","volume":"13","author":"Jensen","year":"2000","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB15","unstructured":"Tommi Junttila. Boolean circuit package version 0.20. http:\/\/www.tcs.hut.fi\/~tjunttil\/circuits\/index.html"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB16","doi-asserted-by":"crossref","unstructured":"O. Kupferman, and M. Y. Vardi. Module checking. In Proceeding of the 8th International Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 75\u201386. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_59"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB17","doi-asserted-by":"crossref","unstructured":"Reinhold Lets. Lemma and model caching in decision procedures for quantified boolean formulas. In Proc. of Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of LNCS, pages 160\u2013175. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45616-3_12"},{"year":"1993","series-title":"Symbolic Model Checking","author":"McMillan","key":"10.1016\/S1571-0661(05)82544-7_BIB18"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB19","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Proceedings of the 14th International Conference on Computer-Aided Verification, volume 2404 of LNCS, pages 250\u2013264. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45657-0_19"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB20","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC\u203201), pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB21","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","article-title":"The control of discrete event systems","volume":"77","author":"Ramadge","year":"1989","journal-title":"Proceedings of the IEEE"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB22","unstructured":"J. Rintanen. Improvements to the evaluation of quantified boolean formulae. In Proceedings of the 16th International Joint Conference on Artificial Intelligence, pages 1192\u20131197, Morgan Kaufmann Publishers, 1999."},{"key":"10.1016\/S1571-0661(05)82544-7_BIB23","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","article-title":"Constructing conditional plans by a theorem prover","volume":"10","author":"Rintanen","year":"1999","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB24","doi-asserted-by":"crossref","unstructured":"W. Thomas Infinite games and verification. In Proceedings of the 14th International Conference on Computer-Aided Verification, volume 2404 of LNCS, pages 58\u201364. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45657-0_5"},{"key":"10.1016\/S1571-0661(05)82544-7_BIB25","doi-asserted-by":"crossref","unstructured":"L. Zhang and S. Malik. Conflict driven learning in a quantified boolean satisfiability solver. In Proceedings of International Conference on Computer Aided Design (ICCAD\u203202), 2002.","DOI":"10.1145\/774572.774637"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825447?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825447?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:10Z","timestamp":1761610150000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105825447"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003]]}},"alternative-id":["S1571066105825447"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)82544-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Symbolic Computational Techniques for Solving Games","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)82544-7","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}