{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T10:55:18Z","timestamp":1768906518365,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319235332","type":"print"},{"value":"9783319235349","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-23534-9_10","type":"book-chapter","created":{"date-parts":[[2015,9,4]],"date-time":"2015-09-04T20:39:52Z","timestamp":1441399192000},"page":"174-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Inherent Vacuity in Lattice Automata"],"prefix":"10.1007","author":[{"given":"Hila","family":"Gonen","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,5]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-39212-2_3","volume-title":"Automata, Languages, and Programming","author":"S Almagor","year":"2013","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 15\u201327. Springer, Heidelberg (2013)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-54830-7_15","volume-title":"Foundations of Software Science and Computation Structures","author":"S Almagor","year":"2014","unstructured":"Almagor, S., Kupferman, O.: Latticed-LTL synthesis in the presence of noisy inputs. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 226\u2013241. Springer, Heidelberg (2014)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-70545-1_23","volume-title":"Computer Aided Verification","author":"R Alur","year":"2008","unstructured":"Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 240\u2013253. Springer, Heidelberg (2008)"},{"key":"10_CR4","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 Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection in linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods Syst. Des. 18(2), 141\u2013162 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"10_CR6","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1215\/S0012-7094-37-00334-X","volume":"3","author":"G Birkhoff","year":"1937","unstructured":"Birkhoff, G.: Rings of sets. Duke Math. J. 3(3), 443\u2013454 (1937)","journal-title":"Duke Math. J."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73368-3_30","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A.: RAT: a tool for the formal analysis of requirements. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proceedings of 16th IEEE Symposium on Logic in Computer Science, pp. 409\u2013420. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932516"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191\u2013206. Springer, Heidelberg (2005)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450\u2013463. Springer, Heidelberg (2000)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-45139-0_3","volume-title":"Model Checking Software","author":"M Chechik","year":"2001","unstructured":"Chechik, M., Devereux, B., Gurfinkel, A.: Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 16\u201336. Springer, Heidelberg (2001)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Chockler, H., Strichman, O.: Easier and more informative vacuity checks. In: Proceedings of 5th International Conference on Formal Methods and Models for Co-Design, pp. 189\u2013198 (2007)","DOI":"10.1109\/MEMCOD.2007.371225"},{"issue":"1","key":"10_CR14","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.fss.2011.07.003","volume":"186","author":"M Ciric","year":"2012","unstructured":"Ciric, M., Ignjatovic, J., Damljanovic, N., Basic, M.: Bisimulations for fuzzy automata. Fuzzy Sets Syst. 186(1), 100\u2013139 (2012)","journal-title":"Fuzzy Sets Syst."},{"key":"10_CR15","volume-title":"Handbook of Weighted Automata","year":"2009","unstructured":"Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Easterbrook, S., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proceedings 23rd Internatioanl Conference on Software Engineering, pp. 411\u2013420. IEEE Computer Society Press (2001)","DOI":"10.1109\/ICSE.2001.919114"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-30494-4_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306\u2013321. Springer, Heidelberg (2004)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-33386-6_4","volume-title":"Automated Technology for Verification and Analysis","author":"S Halamish","year":"2012","unstructured":"Halamish, S., Kupferman, O.: Approximating deterministic lattice automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 27\u201341. Springer, Heidelberg (2012)"},{"issue":"1","key":"10_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2631915","volume":"16","author":"S Halamish","year":"2015","unstructured":"Halamish, S., Kupferman, O.: Minimizing deterministic lattice automata. ACM Trans. Computat. Logic 16(1), 1\u201321 (2015)","journal-title":"ACM Trans. Computat. Logic"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: From Boolean to quantitative notions of correctness. In: Proceedings of 37th ACM Symposium on Principles of Programming Languages, pp. 157\u2013158 (2010)","DOI":"10.1145\/1706299.1706319"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of 36th Design Automation Conference, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"key":"10_CR23","unstructured":"Hussain, A., Huth,M.: On model checking multiple hybrid views. Technical report TR-2004-6, University of Cyprus (2004)"},{"key":"10_CR24","first-page":"935","volume":"17","author":"N Immerman","year":"1988","unstructured":"Immerman, N.: Nondeterministic space is closed under complement. Inf. Comput. 17, 935\u2013938 (1988)","journal-title":"Inf. Comput."},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1016\/S0022-0000(75)80050-X","volume":"11","author":"ND Jones","year":"1975","unstructured":"Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68\u201375 (1975)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11817949_3","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 37\u201351. Springer, Heidelberg (2006)"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-69738-1_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O Kupferman","year":"2007","unstructured":"Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199\u2013213. Springer, Heidelberg (2007)"},{"issue":"2","key":"10_CR28","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Softw. Tools Technol. Transfer 4(2), 224\u2013233 (2003)","journal-title":"Softw. Tools Technol. Transfer"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential time. In: Proceedings of 13th IEEE Symposium on Switching and Automata Theory, pp. 125\u2013129 (1972)","DOI":"10.1109\/SWAT.1972.29"},{"issue":"2","key":"10_CR30","first-page":"269","volume":"23","author":"M Mohri","year":"1997","unstructured":"Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269\u2013311 (1997)","journal-title":"Comput. Linguist."},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-540-27813-9_5","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2004","unstructured":"Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 57\u201369. Springer, Heidelberg (2004)"},{"key":"10_CR32","unstructured":"PROSYD.: The Prosyd project on property-based system design (2007). http:\/\/www.prosyd.org"},{"key":"10_CR33","unstructured":"Roveri, M.: Novel techniques for property assurance. Technical report, PROSYD FP6-IST-507219 (2007)"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"1","key":"10_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Fields of Logic and Computation II"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23534-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T12:44:26Z","timestamp":1748609066000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23534-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319235332","9783319235349"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23534-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"5 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}