TCS / Research / Publications / Simple bounded LTL model checking
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Simple bounded LTL model checking

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},
}

See www.springerlink.com ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.