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. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 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:

@techreport{HUT-TCS-A92,
    address = {Espoo, Finland},
    author = {Timo Latvala and Armin Biere and Keijo Heljanko and Tommi Junttila},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {July},
    number = {A92},
    pages = {16},
    title = {Simple Bounded {LTL} Model Checking},
    type = {Research Report},
    year = {2004},
}

See www.tcs.hut.fi ...

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