Linear Encodings of Bounded LTL Model Checking

Abstract. We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we show how the encodings can be extended to LTL with past operators (PLTL). The generalised encoding is still of linear size, but cannot detect minimal length counterexamples. By using the virtual unrolling technique minimal length counterexamples can be captured, however, the size of the encoding is quadratic in the specification. We also extend virtual unrolling to B

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
• Keywords: BMC Encodings, CORR 2006, Education, Efficient Encodings, Minimal Length Counterexamples