{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:48:44Z","timestamp":1760586524387},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_32","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T18:44:59Z","timestamp":1278873899000},"page":"493-509","source":"Crossref","is-referenced-by-count":27,"title":["Shortest Counterexamples for Symbolic Model Checking of LTL with Past"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-27813-9_8","volume-title":"Computer Aided Verification","author":"M. Awedh","year":"2004","unstructured":"Awedh, M., Somenzi, F.: Proving more properties with bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 96\u2013108. Springer, Heidelberg (2004)"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-36577-X_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedetti","year":"2003","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 18\u201333. Springer, Heidelberg (2003)"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 245\u2013259. Springer, Heidelberg (2004)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: FMSD, vol.\u00a010(1), pp. 47\u201371 (1997)","DOI":"10.1023\/A:1008615614281"},{"key":"32_CR7","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/217474.217565","volume-title":"DAC 1995","author":"E. Clarke","year":"1995","unstructured":"Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: DAC 1995, pp. 427\u2013432. ACM, New York (1995)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: FMSD, vol.\u00a01(2\/3), pp. 275\u2013288 (1992)","DOI":"10.1007\/978-1-4615-3556-0_5"},{"key":"32_CR9","first-page":"995","volume-title":"Handbook of Theoretical Computer Science: Volume B, Formal Methods and Semantics","author":"A. Emerson","year":"1990","unstructured":"Emerson, A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Volume B, Formal Methods and Semantics, pp. 995\u20131072. North-Holland Pub. Co., Amsterdam (1990)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1989","unstructured":"Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398, pp. 409\u2013448. Springer, Heidelberg (1989)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-24732-6_7","volume-title":"Model Checking Software","author":"P. Gastin","year":"2004","unstructured":"Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 92\u2013108. Springer, Heidelberg (2004)"},{"key":"32_CR12","series-title":"IFIP Conference Proceedings","first-page":"3","volume-title":"PSTV 1995","author":"R. Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995. IFIP Conference Proceedings, vol.\u00a038, pp. 3\u201318. Chapman & Hall, Boca Raton (1996)"},{"key":"32_CR13","unstructured":"Groce, A., Kr\u00f6ning, D.: Making the most of BMC counterexamples. In: Biere, A., Strichman, O. (eds.) BMC 2004, pp. 71\u201384 (2004)"},{"key":"32_CR14","unstructured":"The\u00a0VIS Group. VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"32_CR15","unstructured":"Kamp, J.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California at Los Angeles (1968)"},{"key":"32_CR16","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":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 172\u2013183. Springer, Heidelberg (1999)"},{"key":"32_CR18","first-page":"383","volume-title":"LICS 2002","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: LICS 2002, pp. 383\u2013392. IEEE Computer Society, Los Alamitos (2002)"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-540-30579-8_25","volume-title":"VMCAI 2005","author":"T. Latvala","year":"2005","unstructured":"Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: Efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 380\u2013395. Springer, Heidelberg (2005)"},{"key":"32_CR20","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":"32_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"issue":"2\u20133","key":"32_CR22","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2\u20133), 185\u2013204 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. Technical Reports 470, ETH Z\u00fcrich, Computer Systems Institute, 01 (2005)","DOI":"10.1007\/978-3-540-31980-1_32"},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201dMore deterministic\u201d vs. \u201dsmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"32_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 58\u201370. Springer, Heidelberg (2001)"},{"key":"32_CR26","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":"32_CR27","first-page":"332","volume-title":"LICS 1986","author":"M. Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"}],"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-31980-1_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:32:47Z","timestamp":1605742367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}