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 ComputerAided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186–200. SpringerVerlag, 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 CNFformula 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 ComputerAided Design (FMCAD'04)},
editor = {Alan Hu and Andy Martin},
month = {November},
pages = {186200},
publisher = {SpringerVerlag},
series = {Lecture Notes in Computer Science},
title = {Simple bounded {LTL} model checking},
volume = {3312},
year = {2004},
}
