{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:52Z","timestamp":1740028792908,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_7","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"106-122","source":"Crossref","is-referenced-by-count":2,"title":["Sharp Disjunctive Decomposition for Language Emptiness Checking"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"7_CR2","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, UK, June 1986."},{"key":"7_CR3","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"7_CR4","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. P. Kurshan","year":"1994","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994."},{"key":"7_CR5","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium of Logic in Computer Science, pages 267\u2013278, June 1986."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"R. Hojati, H. Touati, R. P. Kurshan, and R. K. Brayton. Efficient \u03c9-regular language containment. In Computer Aided Verification, pages 371\u2013382, Montr\u00e9al, Canada, June 1992.","DOI":"10.1007\/3-540-56496-9_31"},{"issue":"1","key":"7_CR7","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1006\/inco.1995.1055","volume":"118","author":"H. J. Touati","year":"1995","unstructured":"H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for \u03c9-automata using BDD\u2019s. Information and Computation, 118(1):101\u2013109, April 1995.","journal-title":"Information and Computation"},{"key":"7_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"International Colloquium on Automata, Languages, and Programming (ICALP-98)","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten, A. Pnueli, and L.-o. Raviv. Algorithmic verification of linear temporal logic specifications. In International Colloquium on Automata, Languages, and Programming (ICALP-98), pages 1\u201316, Berlin, 1998. Springer. LNCS 1443."},{"issue":"10","key":"7_CR9","doi-asserted-by":"crossref","first-page":"1225","DOI":"10.1109\/43.875347","volume":"19","author":"A. Xie","year":"2000","unstructured":"A. Xie and P. A. Beerel. Implicit enumeration of strongly connected components and an application to formal verification. IEEE Transactions on Computer-Aided Design, 19(10): 1225\u20131230, October 2000.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-40922-X_4","volume-title":"Formal Methods in Computer Aided Design","author":"R. Bloem","year":"2000","unstructured":"R. Bloem, H. N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in nlogn symbolic steps. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 37\u201354. Springer-Verlag, November 2000. LNCS 1954."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y Vardi. Freedom, weakness, and determinism: From linear-time to branching-time. In Proc. 13th IEEE Symposium on Logic in Computer Science, June 1998.","DOI":"10.1109\/LICS.1998.705645"},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Eleventh Conference on Computer Aided Verification (CAV\u201999)","author":"R. Bloem","year":"1999","unstructured":"R. Bloem, K. Ravi, and F Somenzi. Efficient decision procedures for model checking of linear time logic properties. In N. Halbwachs and D. Peled, editors, Eleventh Conference on Computer Aided Verification (CAV\u201999), pages 222\u2013235. Springer-Verlag, Berlin, 1999. LNCS 1633."},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-44685-0_31","volume-title":"International Conference on Concurrency Theory (CONCUR01)","author":"C. Wang","year":"2001","unstructured":"C. Wang, R. Bloem, G. D. Hachtel, K. Ravi, and F Somenzi. Divide and compose: SCC refinement for language emptiness. In International Conference on Concurrency Theory (CONCUR01), pages 456\u2013471, Berlin, August 2001. Springer-Verlag. LNCS 2154."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi. A state space decomposition algorithm for approximate FSM traversal. In Proceedings of the European Conference on Design Automation, pages 137\u2013141, Paris, France, February 1994.","DOI":"10.1109\/EDTC.1994.326885"},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Eighth Conference on Computer Aided Verification (CAV\u201996)","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV\u201996), pages 428\u2013432. Springer-Verlag, Rutgers University, 1996. LNCS 1102."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"D. L. Dill. What\u2019s between simulation and formal verification? In Proceedings of the Design Automation Conference, pages 328\u2013329, San Francisco, CA, June 1998.","DOI":"10.1145\/277044.277138"},{"key":"7_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer Aided Design","author":"K. Ravi","year":"2000","unstructured":"K. Ravi, R. Bloem, and F. Somenzi. A comparative study of symbolic algorithms for the computation of fair cycles. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 143\u2013160. Springer-Verlag, November 2000. LNCS 1954."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:24:52Z","timestamp":1739993092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}