{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T09:06:28Z","timestamp":1769850388611,"version":"3.49.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,2,15]],"date-time":"2005-02-15T00:00:00Z","timestamp":1108425600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10009-004-0179-0","type":"journal-article","created":{"date-parts":[[2005,2,14]],"date-time":"2005-02-14T08:17:58Z","timestamp":1108369078000},"page":"118-128","source":"Crossref","is-referenced-by-count":23,"title":["Symbolic computational techniques for solving games"],"prefix":"10.1007","volume":"7","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]},{"given":"Wonhong","family":"Nam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,15]]},"reference":[{"key":"179_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, de Alfaro L, Henzinger T, Mang F (1999) Automating modular verification. In: Proceedings of the 10th international conference on concurrency theory. Lecture notes in computer science, vol 1664. Springer, Berlin Heidelberg New York, pp 82\u201397","DOI":"10.1007\/3-540-48320-9_8"},{"key":"179_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL \u201905, Long Beach, California, USA. ACM Press, pp 98\u2013109. ISBN 1-58113-830-X, DOI http:\/\/doi.acm.org\/10.1145\/1040305.1040314","DOI":"10.1145\/1047659.1040314"},{"key":"179_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/585265.585270","volume":"49","author":"Alur","year":"2002","unstructured":"Alur R, Henzinger TA, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):1\u201342","journal-title":"J ACM"},{"key":"179_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S (1998) Mocha: modularity in model checking. In: Proceedings of the 10th internationall conference on computer-aided verification. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 521\u2013525","DOI":"10.1007\/BFb0028774"},{"key":"179_CR5","unstructured":"Arnold A, Niwinski D (2001) Rudiments of \u03bc-calculus. Elsevier, Amsterdam"},{"key":"179_CR6","unstructured":"Bertoli P, Cimatti A, Pistore M, Roveri M, Traverso P (2001) MBP: a model-based planner. In: Proceedings of the IJCAI-2001 workshop on Planning under Uncertainty and Incomplete Information, Seattle, USA, August 2001, pp 93\u201397"},{"key":"179_CR7","doi-asserted-by":"crossref","unstructured":"Biere A (1997) \u03bccke \u2013 efficient \u03bc-calculus model checking. In: Proceedings of the 9th internationall conference on computer-aided verification. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 468\u2013471","DOI":"10.1007\/3-540-63166-6_50"},{"key":"179_CR8","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the internationall conference on tools and algorithms for the analysis and construction of systems (TACAS\u201999). Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"179_CR9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"179_CR10","doi-asserted-by":"crossref","unstructured":"Chakrabarti A, de Alfaro L, Henzinger TA, Jurdzinski M, Mang FYC (2002) Interface compatibility checking for software modules. In: Proceedings of the 14th internationall conference on computer-aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 428\u2013441","DOI":"10.1007\/3-540-45657-0_35"},{"key":"179_CR11","unstructured":"Church A (1963) Logic, arithmetics, and automata. In: Proceedings of the international congress of mathematicians, 1962, Institut Mittag-Leffler, Djursholm, Sweden, pp 23\u201335"},{"key":"179_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia E, Narizzano M, Tacchella A (2001) QUBE: A system for deciding quantified boolean formulas satisfiability. In: Proceedings of the international joint conference on automated reasoning (IJCAR\u201901), pp 364\u2013369","DOI":"10.1007\/3-540-45744-5_27"},{"key":"179_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT solver. In: Proceedings of Design Automation and Test in Europe (DATE\u201902), pp 142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"179_CR14","doi-asserted-by":"crossref","unstructured":"Gupta A, Ganai M, Wang C, Yang Z, Ashar PN (2003) Learning from BDDs in SAT-based bounded model checking. In: Proceedings of the 40th conference on Design automation (DAC \u201903), Anaheim CA, USA. ACM Press, pp 824\u2013829. ISBN 1-58113-688-9, DOI http:\/\/doi.acm.org\/10.1145\/775832.776040","DOI":"10.1109\/DAC.2003.1219133"},{"key":"179_CR15","doi-asserted-by":"crossref","unstructured":"Hill J, Szewczyk R, Woo A, Hollar S, Culler DE, Pister KSJ (2000) System Architecture Directions for Networked Sensors. Architectural Support for Programming Languages and Operating Systems, pp 93\u2013104. citeseer.ist.psu.edu\/382595.html","DOI":"10.1145\/378993.379006"},{"key":"179_CR16","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1613\/jair.649","volume":"13","author":"Jensen","year":"2000","unstructured":"Jensen R, Veloso M (2000) OBDD-based universal planning for synchronized agents in non-deterministic domains. J Artif Intell Res 13:189\u2013226","journal-title":"J Artif Intell Res"},{"key":"179_CR17","unstructured":"Junttila T (2003) Boolean circuit package version 0.20. http:\/\/www.tcs.hut.fi\/\u223ctjunttil\/circuits\/index.html"},{"key":"179_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (1996) Module checking. In: Proceedings of the 8th internationall conference on computer-aided verification. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 75\u201386","DOI":"10.1007\/3-540-61474-5_59"},{"key":"179_CR19","doi-asserted-by":"crossref","unstructured":"Lets R (2002) Lemma and model caching in decision procedures for quantified boolean formulas. In: Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. Lecture notes in computer science, vol 2381. Springer, Berlin Heidelberg New York, pp 160\u2013175","DOI":"10.1007\/3-540-45616-3_12"},{"key":"179_CR20","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Dordrecht","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"179_CR21","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer-aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"179_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th conference on design automation (DAC\u201901), pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"179_CR23","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77:81\u201398","journal-title":"Proc IEEE"},{"key":"179_CR24","unstructured":"Rintanen J (1999) Improvements to the evaluation of quantified boolean formulae. In: Proceedings of the 16th international joint conference on artificial intelligence. Morgan Kaufmann, San Francisco, pp 1192\u20131197"},{"key":"179_CR25","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"Rintanen","year":"1999","unstructured":"Rintanen J (1999) Constructing conditional plans by a theorem prover. J Artif Intell Res 10:323\u2013352","journal-title":"J Artif Intell Res"},{"key":"179_CR26","doi-asserted-by":"crossref","unstructured":"Thomas W (2002) Infinite games and verification. In: Proceedings of the 14th internationall conference on computer-aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 58\u201364","DOI":"10.1007\/3-540-45657-0_5"},{"key":"179_CR27","doi-asserted-by":"crossref","unstructured":"Wallmeier N, H\u00fctten P, Thomas W (2003) Symbolic synthesis of finite-state controllers for request-response specifications. In: Proceedings of the 8th internationall conference on the implementation and application of automata (CIAA\u201903). Lecture notes in computer science, vol 2759. Springer, Berlin Heidelberg New York, pp 11\u201322","DOI":"10.1007\/3-540-45089-0_3"},{"key":"179_CR28","doi-asserted-by":"crossref","unstructured":"Zhang L, Malik S (2002) Conflict driven learning in a quantified Boolean Satisfiability solver. In: Proceedings of the 2002 IEEE\/ACM international conference on Computer-aided design (ICCAD \u201902), San Jose, California. ACM Press, pp 442\u2013449. ISBN 0-7803-7607-2, DOI http:\/\/doi.acm.org\/10.1145\/774572.774637","DOI":"10.1145\/774572.774637"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0179-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0179-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0179-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:20Z","timestamp":1559100320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0179-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2,15]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["179"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0179-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2,15]]}}}