{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,6]],"date-time":"2025-12-06T04:33:29Z","timestamp":1764995609549},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_16","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"191-206","source":"Crossref","is-referenced-by-count":37,"title":["Regular Vacuity"],"prefix":"10.1007","author":[{"given":"Doron","family":"Bustan","sequence":"first","affiliation":[]},{"given":"Alon","family":"Flaisher","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Accellera, http:\/\/www.accellera.org"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R. Armon","year":"2003","unstructured":"Armon, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection for linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 211\u2013296. Springer, Heidelberg (2002)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"issue":"2","key":"16_CR5","first-page":"141","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. FMSD\u00a018(2), 141\u2013162 (2001)","journal-title":"FMSD"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem (1996)","DOI":"10.1007\/978-3-642-59207-2"},{"key":"16_CR7","unstructured":"B\u00fcchi, J.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, Stanford, pp. 1\u201312 (1962)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427\u2013432 (1995)","DOI":"10.1145\/217474.217565"},{"key":"16_CR9","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-46011-X_4","volume-title":"Developments in Language Theory","author":"T. Eiter","year":"2002","unstructured":"Eiter, T., Gottlob, G., Schwentick, T.: Second-order logic over strings: Regular and non-regular fragments. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol.\u00a02295, pp. 37\u201356. Springer, Heidelberg (2002)"},{"key":"16_CR11","first-page":"194","volume":"18","author":"M. Fischer","year":"1979","unstructured":"Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. JCSS\u00a018, 194\u2013211 (1979)","journal-title":"JCSS"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"16_CR13","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, Boca Raton (1995)"},{"issue":"2","key":"16_CR14","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/972639.972646","volume":"51","author":"G. Gottlob","year":"2000","unstructured":"Gottlob, G., Kolaitis, P.G., Schwentick, T.: Existential second-order logic over graphs: Charting the tractability frontier. JACM\u00a051(2), 312\u2013362 (2000)","journal-title":"JACM"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: 5th FMCAD. LNCS, vol.\u00a02212, pp. 306\u2013321 (2004)","DOI":"10.1007\/978-3-540-30494-4_22"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-540-24730-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 451\u2013466. Springer, Heidelberg (2004)"},{"issue":"1\u20133","key":"16_CR17","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J. Henriksen","year":"1999","unstructured":"Henriksen, J., Thiagarajan, P.: Dynamic linear time temporal logic. Annals of Pure and Applied Logic\u00a096(1\u20133), 187\u2013207 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"16_CR18","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"issue":"2","key":"16_CR19","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"STTT"},{"key":"16_CR20","unstructured":"Kurshan, R.: FormalCheck User\u2019s Manual. Cadence Design, Inc. (1998)"},{"key":"16_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Computer Aided Verification","author":"M. Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 485\u2013499. Springer, Heidelberg (2002)"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS\u00a0141, 1\u201335 (1969)","journal-title":"Transaction of the AMS"},{"key":"16_CR24","unstructured":"Savelsberg, M., van emde Boas, P.: Bounded tiling, an alternative to satisfiability. In: 2nd Frege conference, pp. 354\u2013363. Akademya Verlag (1984)"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. Journal ACM\u00a032, 733\u2013749 (1985)","journal-title":"Journal ACM"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"M. Vardi","year":"1994","unstructured":"Vardi, M.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 575\u2013597. Springer, Heidelberg (1994)"},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:50:25Z","timestamp":1605642625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11560548_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}