{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:49Z","timestamp":1725488929070},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_2","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"16-30","source":"Crossref","is-referenced-by-count":12,"title":["BDD-Based Decision Procedures for $$ \\mathcal{K} $$"],"prefix":"10.1007","author":[{"given":"Guoqiang","family":"Pan","sequence":"first","affiliation":[]},{"given":"Ulrike","family":"Sattler","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"2_CR1","unstructured":"H. R. Andersen. An introduction to binary decision diagrams. Technical report, Department of Information Technology, Technical University of Denmark, 1998."},{"key":"2_CR2","unstructured":"C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. Tree-based heuristics in modal theorem proving. In Proceedings of the ECAI\u20192000, 2000."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45422-5","volume-title":"Proc. of IJCAR-01","author":"F. Baader","year":"2001","unstructured":"F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfiability. In Proc. of IJCAR-01, volume 2083 of LNCS. Springer Verlag, 2001."},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"Proc. of CAV-94","author":"I. Beer","year":"1994","unstructured":"I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. of CAV-94, volume 818 of LNCS, pages 182\u2013193, 1994."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. D. Rijke, Y. Venema, and M. D. Rijke. Modal logic. Cambridge University Press, 2001.","DOI":"10.1017\/CBO9781107050884"},{"issue":"8","key":"2_CR6","first-page":"677","volume":"-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, Vol. C-35(8):677\u2013691, August 1986.","journal-title":"Vol. C"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Infomation and Computation, 98(2):142\u2013170, 1992.","journal-title":"Infomation and Computation"},{"key":"2_CR8","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Int. Conf. on VLSI, pages 49\u201358, 1991."},{"issue":"4","key":"2_CR9","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A new symbolic model checker. Int. Journal on Software Tools for Technology Transfer, 2(4):410\u2013425, 2000.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"2_CR10","unstructured":"R. Dyckhoff, editor. Proceedings of TABLEAUX 2000, volume 1847 of LNAI. Springer Verlag, 2000."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"D. Geist and H. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. of the sixth Int. Conf. on CAV, pages 299\u2013310, 1994.","DOI":"10.1007\/3-540-58179-0_63"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In IJCAR, pages 347\u2013363, 2001.","DOI":"10.1007\/3-540-45744-5_26"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1006\/inco.1999.2850","volume":"162","author":"F. Giunchiglia","year":"2000","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedure-the case study of modal K(m). Infomation and Computation, 162:158\u2013178, 2000.","journal-title":"Infomation and Computation"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Y. Halpern","year":"1992","unstructured":"J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319\u2013379, 1992.","journal-title":"Artificial Intelligence"},{"key":"2_CR15","volume-title":"Technical report","author":"A. Heuerding","year":"1996","unstructured":"A. Heuerding and S. Schwendimann. A benchmark method for the propositional modal logics K, KT, S4. Technical report, Universit\u00e4t Bern, Switzerland, 1996."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"U. Hustadt and R. Schmidt. MSPASS: modal reasoning by translation and first order resolution. In [10], pages 67\u201371.","DOI":"10.1007\/10722086_7"},{"key":"2_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-49519-3_19","volume-title":"Proc. of FMCAD\u201998","author":"G. Kamhi","year":"1998","unstructured":"G. Kamhi, L. Fix, and Z. Binyamini. Symbolic model checking visualization. In Proc. of FMCAD\u201998, volume 1522 of LNCS, pages 290\u2013303. Springer Verlag, November 1998."},{"issue":"3","key":"2_CR18","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467\u2013480, 1977.","journal-title":"SIAM J. Comput."},{"key":"2_CR19","unstructured":"F. Massacci and F. M. Donini. Design and results of TANCS-00. In [10], pages 52\u201356."},{"key":"2_CR20","series-title":"Lect Notes Comput Sci","first-page":"73","volume-title":"FMCAD2000","author":"I.-H. Moon","year":"2000","unstructured":"I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block trianglular form and conjunction schedule in image computation. In W. H. Jr. and S. Johnson, editors, FMCAD2000, volume 1954 of LNCS, pages 73\u201390. Springer Verlag, 2000."},{"key":"2_CR21","unstructured":"H. Ohlbach, A. Nonnengart, M. de Rijke, and D. Gabbay. Encoding two-valued non-classical logics in classical logic. In J. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier, 1999."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"P. F. Patel-Schneider and I. Horrocks. DLP and FaCT. In Proc. of TABLEAUX-99, volume 1397 of LNAI, pages 19\u201323. Springer Verlag, 1999.","DOI":"10.1007\/3-540-48754-9_3"},{"issue":"2","key":"2_CR23","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"V. Pratt","year":"1980","unstructured":"V. Pratt. A near-optimal method for reasoning about action. Journal of Computer and System Sciences, 20(2):231\u2013254, 1980.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR24","unstructured":"R. Ranjan, A. Aziz, R. Brayton, B. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In Proceedings of IEEE\/ACM International Workshop on Logic Synthesis, 1995."},{"key":"2_CR25","unstructured":"F. Somenzi. CUDD: CU decision diagram package, 1998."},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliffe","year":"2001","unstructured":"G. Sutcliffe and C. Suttner. Evaluating general purpose automated theorem proving systems. Artificial intelligence, 131:39\u201354, 2001.","journal-title":"Artificial intelligence"},{"key":"2_CR27","unstructured":"A. Tacchella. *SAT system description. In Collected Papers from the International Description Logics Workshop (DL\u201999). CEUR, 1999."},{"key":"2_CR28","unstructured":"J. van Benthem. Modal Logic and Classical Logic. Bibliopolis, 1983."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"M. Vardi. What makes modal logic so robustly decidable? In N. Immerman and P. Kolaitis, editors, Descriptive Complexity and Finite Models, pages 149\u2013183. American Mathematical Society, 1997.","DOI":"10.1090\/dimacs\/031\/05"},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/371316.371511","volume":"2","author":"A. Voronkov","year":"2001","unstructured":"A. Voronkov. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Computational Logic, 2(2):182\u2013215, 2001.","journal-title":"Computational Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:55:42Z","timestamp":1556754942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}