Simple bounded LTL model checking

Reference:

Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186–200. Springer-Verlag, November 2004.

Abstract:

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.

Keywords:

LTL, Bounded Model Checking, NuSMV

Suggested BibTeX entry:

@inproceedings{LatBieHelJun:FMCAD04,
    author = {Timo Latvala and Armin Biere and Keijo Heljanko and Tommi Junttila},
    booktitle = {Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04)},
    editor = {Alan Hu and Andy Martin},
    month = {November},
    pages = {186--200},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Simple bounded {LTL} model checking},
    volume = {3312},
    year = {2004},
}