{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T12:15:13Z","timestamp":1767183313065,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_8","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"82-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":44,"title":["Vacuity Detection in Temporal Model Checking"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"D. Beaty and R. Bryant. Formally verifying a microprocessor using a simulation methodology. In Proc. 31st DAC, pp. 596\u2013602. IEEE Computer Society, 1994.","DOI":"10.1145\/196244.196575"},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Proc. 9th CAV","author":"I. Beer","year":"1997","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In Proc. 9th CAV, LNCS 1254, pp. 279\u2013290, 1997."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 11th CAV","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 Proc. 11th CAV, LNCS, 1999."},{"key":"8_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/BFb0013029","volume-title":"Proc. Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency","author":"E. M. Clarke","year":"1988","unstructured":"E. M. Clarke and I. A. Draghicescu. Expressibility results for linear-time and branching-time logics. In Proc. Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, LNCS 354, pp. 428\u2013437, 1988."},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Workshop on Logic of Programs","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pp. 52\u201371, 1981."},{"issue":"2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"Decade of Concurrency-Reflections and Perspectives (Proceedings of REX School)","author":"E. M. Clarke","year":"1993","unstructured":"E. M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In Decade of Concurrency-Reflections and Perspectives (Proceedings of REX School), LNCS 803, pp. 124\u2013175, 1993."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd DAC, pp. 427\u2013432. IEEE Computer Society, 1995.","DOI":"10.1109\/DAC.1995.249985"},{"key":"8_CR9","unstructured":"E. Clarke. Private communication, 1997."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th FOCS, pp. 368\u2013377, White Plains, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1987","unstructured":"E. A. Emerson and C.L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, pp. 997\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"N. Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"8_CR14","series-title":"Lect Notes Comput Sci","volume-title":"10th CHARME","author":"S. Katz","year":"1999","unstructured":"S. Katz, D. Geist, and O. Grumberg. \u201cHave I written enough properties ?\u201d a method of comparison between specification and implementation. In 10th CHARME, LNCS, 1999."},{"key":"8_CR15","unstructured":"R. P. Kurshan. FormalCheck User\u2019s Manual. Cadence Design, Inc., 1998."},{"key":"8_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-60218-6_31","volume-title":"Proc. 6th CONCUR","author":"O. Kupferman","year":"1995","unstructured":"O. Kupferman and M. Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th CONCUR, LNCS 962, pp. 408\u2013422, 1995."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: from linear-time to branching-time. In Proc. 13th LICS, pp. 81\u201392, 1998.","DOI":"10.1109\/LICS.1998.705645"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y. Vardi. Relating linear and branching model checking. In PROCOMET, pp. 304\u2013326, 1998. Chapman & Hall.","DOI":"10.1007\/978-0-387-35358-6_21"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D. E. Muller","year":"1995","unstructured":"D. E. Muller and P. E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69\u2013107, 1995.","journal-title":"Theoretical Computer Science"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"B. Plessier and C. Pixley. Formal verification of a commercial serial bus interface. In Proc. of 14th Annual IEEE International Phoenix Conf. on Computers and Communicat ions, pp. 378\u2013382, March 1995.","DOI":"10.1109\/PCCC.1995.472465"},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symp. on Programming","author":"J. P. Queille","year":"1981","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, pp. 337\u2013351, LNCS 137, 1981."},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th STOC, pp. 240\u2013251, 1985.","DOI":"10.1145\/22145.22173"},{"key":"8_CR26","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LICS, pp. 322\u2013331, 1986."},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182\u2013221, April 1986.","journal-title":"Journal of Computer and System Science"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:16:20Z","timestamp":1739992580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"3 June 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}