Reference:
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan J. Hu and Andrew K. Martin, editors, Formal Methods in Computer-Aided Design 2004, 5th International Conference FMCAD'04, Austin, Texas, USA, volume 3312 of Lecture Notes in Computer Science, pages 186–200. Springer, nov 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 = {Formal Methods in Computer-Aided Design 2004, 5th International Conference FMCAD'04, Austin, Texas, USA},
editor = {Alan J. Hu and Andrew K. Martin},
month = {nov},
pages = {186-200},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Simple bounded {LTL} model checking},
volume = {3312},
year = {2004},
}
|