Simple Bounded LTL Model Checking

We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-formula has a linear number of variables and clauses.

• Type: Conference
• Year: 2004
• Where: FMCAD
• Authors: Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
• Keywords: FMCAD 2004, Linear, Model Checking Problem, Simple Translation