{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T10:29:34Z","timestamp":1776940174646,"version":"3.51.4"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1023\/a:1008779610539","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"141-163","source":"Crossref","is-referenced-by-count":94,"title":["Efficient Detection of Vacuity in Temporal Model Checking"],"prefix":"10.1007","volume":"18","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cindy","family":"Eisner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoav","family":"Rodeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"315473_CR1","volume-title":"Entailment: The Logic of Relevance and Necessity","author":"A.R. Anderson","year":"1975","unstructured":"A.R. Anderson and N.D. Belnap, Jr., Entailment: The Logic of Relevance and Necessity, Princeton University Press, Princeton, Vol. 1, 1975, Vol. 2 (with J. Michael Dunn), 1992."},{"key":"315473_CR2","doi-asserted-by":"crossref","unstructured":"D. Beatty and R. Bryant, \u201cFormally verifying a microprocessor using a simulation methodology,\u201d in Design Automation Conference '94, pp. 596\u2013602.","DOI":"10.1145\/196244.196575"},{"key":"315473_CR3","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver, \u201cRuleBase: An industry-oriented formal verification tool,\u201d in Proc. 33rd Design Automation Conference 1996, pp. 655\u2013660.","DOI":"10.1109\/DAC.1996.545656"},{"key":"315473_CR4","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, \u201cEfficient detection of vacuity in ACTL formulas,\u201d in CAV '97, LNCS 1254, pp. 279\u2013290.","DOI":"10.1007\/3-540-63166-6_28"},{"issue":"1\u20132","key":"315473_CR5","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, \u201cCharacterizing finite Kripke structures in propositional temporal logic,\u201d Theoretical Computer Science, Vol. 59, No. 1\u20132, 1988, pp. 115\u2013131.","journal-title":"Theoretical Computer Science"},{"key":"315473_CR6","unstructured":"F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone, \u201cOn ACTL Formulas Having Deterministic Counterexamples,\u201d University of Technology Vienna Technical Report INFSYS RR-1843-99-01."},{"key":"315473_CR7","first-page":"52","volume-title":"Proc. Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using Branching Time Temporal Logic,\u201d in Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131 (Springer, Berlin, 1981) pp. 52\u201371."},{"key":"315473_CR8","unstructured":"E.M. Clarke and E.A. Emerson, \u201cCharacterizing properties of parallel programs as fixed-point,\u201d in Seventh International Colloquium on Automata, Languages, and Programming, Vol. 85 of LNCS, 1981."},{"key":"315473_CR9","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, K. McMillan, and X. Zhao, \u201cEfficient generation of counterexamples and witnesses in symbolic model checking,\u201d in Design Automation Conference 1995, pp. 427\u2013432.","DOI":"10.1109\/DAC.1995.249985"},{"key":"315473_CR10","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999."},{"issue":"1","key":"315473_CR11","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern, \u201c'Sometimes' and' Not Never' revisited: On branching versus linear time temporal logic,\u201d Journal of the Association for Computing Machinery, Vol. 33, No. 1, pp. 151\u2013178, 1986.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"315473_CR12","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D. Long, \u201cModel checking and modular verification,\u201d in J.C.M. Baeten and J.F. Groote, (Eds), Procceedings of CONCUR '91: 2nd International Conference on Concurrency Theory, Vol. 527 of LNCS, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"315473_CR13","doi-asserted-by":"crossref","unstructured":"R. Hojati, R.K. Brayton, and R.P. Kurshan, \u201cBDD-based debugging of designs using language containment and fair CTL,\u201d in CAV '93, pp. 41\u201358.","DOI":"10.1007\/3-540-56922-7_5"},{"key":"315473_CR14","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi, \u201cVacuity Detection in Temporal Model Checking,\u201d in CHARME 99, LNCS 1703, Springer-Verlag 1999.","DOI":"10.1007\/3-540-48153-2_8"},{"key":"315473_CR15","doi-asserted-by":"crossref","unstructured":"R. Kurshan, Analysis of Discrete Event Coordination, LNCS 1990.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"315473_CR16","unstructured":"D. Long, \u201cModel Checking, Abstraction and Compositional Verification,\u201d Ph.D. Thesis, CMU, 1993."},{"key":"315473_CR17","unstructured":"Edwin D. Mares, \u201cRelevance Logic,\u201d The Stanford Encyclopedia of Philosophy, (Fall 1999 Edition), Edward N. Zalta (Ed.), URL=http:\/\/plato.stanford.edu\/archives\/win1999\/entries\/logic-relevance\/."},{"key":"315473_CR18","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"315473_CR19","unstructured":"R. Milner. \u201cAn algebraic definition of simulation between programs,\u201d in Proc. 2nd International Joint Conference on Artificial Intelligence, British Computer Society, September 1971."},{"key":"315473_CR20","doi-asserted-by":"crossref","unstructured":"B. Plessier and C. Pixley, \u201cFormal verification of a commercial serial bus interface,\u201d in International Phoenix Conference on Computers and Communications, 1995, pp. 378\u2013382.","DOI":"10.1109\/PCCC.1995.472465"},{"key":"315473_CR21","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, \u201cA temporal logic of concurrent programs,\u201d Theoretical Computer Science, Vol. 13, pp. 45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"315473_CR22","unstructured":"A. Pnueli, \u201cLinear and Branching Structures in the semantics and logics of reactive systems,\u201d in Proc. 12th Int. Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, Springer-Verlag, 1985."},{"key":"315473_CR23","doi-asserted-by":"crossref","unstructured":"A. Pnueli, N. Shankar, and E. Singerman, \u201cFair synchronous transition systems and their liveness proofs,\u201d in A.P. Ravn and H. Rischel, (Eds), FTRTFT 98: 5th International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science, Springer-Verlag, 1998.","DOI":"10.1007\/BFb0055348"},{"key":"315473_CR24","unstructured":"A. Pnueli, Question from the Audience, CAV '97."},{"key":"315473_CR25","unstructured":"G. Shurek and O. Grumberg, \u201cThe computer-aided modular framework\u2014motivation, solutions and evaluation criteria,\u201d in Workshop on Computer Aided Verification, 1990."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008779610539.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008779610539\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008779610539.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:20:13Z","timestamp":1754421613000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008779610539"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["315473"],"URL":"https:\/\/doi.org\/10.1023\/a:1008779610539","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}