{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T23:55:15Z","timestamp":1770767715912,"version":"3.50.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2006,11,15]],"date-time":"2006-11-15T00:00:00Z","timestamp":1163548800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","award":["211025"],"award-info":[{"award-number":["211025"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","award":["109539"],"award-info":[{"award-number":["109539"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","award":["213113"],"award-info":[{"award-number":["213113"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider the problem of bounded model checking (BMC) for linear temporal\nlogic (LTL). We present several efficient encodings that have size linear in\nthe bound. Furthermore, we show how the encodings can be extended to LTL with\npast operators (PLTL). The generalised encoding is still of linear size, but\ncannot detect minimal length counterexamples. By using the virtual unrolling\ntechnique minimal length counterexamples can be captured, however, the size of\nthe encoding is quadratic in the specification. We also extend virtual\nunrolling to Buchi automata, enabling them to accept minimal length\ncounterexamples.\n  Our BMC encodings can be made incremental in order to benefit from\nincremental SAT technology. With fairly small modifications the incremental\nencoding can be further enhanced with a termination check, allowing us to prove\nproperties with BMC. Experiments clearly show that our new encodings improve\nperformance of BMC considerably, particularly in the case of the incremental\nencoding, and that they are very competitive for finding bugs. An analysis of\nthe liveness-to-safety transformation reveals many similarities to the BMC\nencodings in this paper. Using the liveness-to-safety translation with\nBDD-based invariant checking results in an efficient method to find shortest\ncounterexamples that complements the BMC-based approach.<\/jats:p>","DOI":"10.2168\/lmcs-2(5:5)2006","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:30:05Z","timestamp":1164274205000},"source":"Crossref","is-referenced-by-count":108,"title":["Linear Encodings of Bounded LTL Model Checking"],"prefix":"10.46298","volume":"Volume 2, Issue 5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"first","affiliation":[{"name":"Institute for Formal Models and Verification, Johannes Kepler University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4547-2701","authenticated-orcid":false,"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[{"name":"Laboratory for Theoretical Computer Science, Helsinki University of Technology"}]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[{"name":"Laboratory for Theoretical Computer Science, Helsinki University of Technology"}]},{"given":"Timo","family":"Latvala","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign"}]},{"given":"Viktor","family":"Schuppan","sequence":"additional","affiliation":[{"name":"Computer Systems Institute, ETH Zentrum"}]}],"member":"25203","published-online":{"date-parts":[[2006,11,15]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2236\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2236\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:10:18Z","timestamp":1681243818000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2236"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11,15]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-2(5:5)2006","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0611029","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0611029","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,11,15]]},"article-number":"2236"}}