{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:46:06Z","timestamp":1725561966060},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_43","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:00:15Z","timestamp":1280761215000},"page":"591-606","source":"Crossref","is-referenced-by-count":12,"title":["From Complementation to Certification"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2\/3","key":"43_CR1","first-page":"171","volume":"10","author":"R. Bahar","year":"1997","unstructured":"Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi\", F.: Algebraic decision diagrams and their applications. FMSD\u00a010(2\/3), 171\u2013206 (1997)","journal-title":"FMSD"},{"key":"43_CR2","series-title":"Lecture Notes in Computer Science","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":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 37\u201354. Springer, Heidelberg (2000)"},{"key":"43_CR3","first-page":"1","volume-title":"Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"key":"43_CR4","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: A simplified approach. Journal of Computer and System Sciences\u00a08, 117\u2013141 (1974)","journal-title":"Journal of Computer and System Sciences"},{"key":"43_CR5","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc. 1st LICS, pp. 267\u2013278 (1986)"},{"key":"43_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"key":"43_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"43_CR8","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: Proc. 14th SODA, pp. 573\u2013582 (2003)"},{"key":"43_CR9","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, August 1995, pp. 3\u201318. Chapman & Hall, Boca Raton (1995)"},{"key":"43_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/10720246_18","volume-title":"Recent Advances in AI Planning","author":"G. Giacomo De","year":"2000","unstructured":"De Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning for temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol.\u00a01809, pp. 226\u2013238. Springer, Heidelberg (2000)"},{"key":"43_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1997","unstructured":"Hardin, R.H., Kurshan, R.P., Shukla, S.K., Vardi, M.Y.: A new heuristic for bad cycle detection using BDDs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 268\u2013278. Springer, Heidelberg (1997)"},{"key":"43_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R. Hojati","year":"1993","unstructured":"Hojati, R., Touati, H., Kurshan, R., Brayton, R.: Efficient \u03c9-regula language containment. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, Springer, Heidelberg (1993)"},{"key":"43_CR13","doi-asserted-by":"crossref","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358\u2013367 (1991)","DOI":"10.1109\/SFCS.1991.185391"},{"key":"43_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"key":"43_CR15","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: The complexity of verification. In: 26th STOC, pp. 365\u2013371 (1994)","DOI":"10.1145\/195058.195194"},{"key":"43_CR16","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)"},{"issue":"3","key":"43_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal methods in System Design"},{"issue":"2","key":"43_CR18","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2001","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. on Computational Logic\u00a02001(2), 408\u2013429 (2001)","journal-title":"ACM Trans. on Computational Logic"},{"key":"43_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-44659-1_26","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Merz","year":"2000","unstructured":"Merz, S.: Weak alternating automata in Isabelle\/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 423\u2013440. Springer, Heidelberg (2000)"},{"key":"43_CR20","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoretical Computer Science\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science"},{"key":"43_CR21","volume-title":"Complementation is more difficult with automata on infinite words","author":"M. Michel","year":"1988","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)"},{"key":"43_CR22","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by \u2200-automata. In: Proc. Proc. 14th POPL, pp. 1\u201312 (1987)","DOI":"10.1145\/41625.41626"},{"key":"43_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, Berlin (January 1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"1","key":"43_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM TOPLAS\u00a06(1), 68\u201393 (1984)","journal-title":"ACM TOPLAS"},{"key":"43_CR25","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":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 2\u201313. Springer, Heidelberg (2001)"},{"key":"43_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. 24th POPL, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"43_CR27","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":"D. Peled","year":"2001","unstructured":"Peled, D., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 292\u2013304. Springer, Heidelberg (2001)"},{"key":"43_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45139-0_1","volume-title":"Model Checking Software","author":"D. Peled","year":"2001","unstructured":"Peled, D., Zuck, L.D.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 1\u201314. Springer, Heidelberg (2001)"},{"key":"43_CR29","series-title":"Lecture Notes in Computer Science","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":"Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"key":"43_CR30","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: 29th FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"43_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"43_CR32","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Satefy, liveness and fairness in temporal logic. Formal Aspects of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"43_CR33","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"43_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Tasiran","year":"1995","unstructured":"Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using nondeterministic \u03c9-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"issue":"1","key":"43_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"issue":"1-2","key":"43_CR36","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1-2), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T03:18:45Z","timestamp":1559359125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}