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. bounded model checking, LTL, linear translation, NuSMV. © Springer-Verlag 2004.
CITATION STYLE
Latvala, T., Biere, A., Heljanko, K., & Junttila, T. (2004). Simple bounded LTL model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 186–200. https://doi.org/10.1007/978-3-540-30494-4_14
Mendeley helps you to discover research relevant for your work.