TCS / Research / Publications / A New Unfolding Approach to LTL Model Checking
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

A New Unfolding Approach to LTL Model Checking

Reference:

Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. Series A: Research Report 60, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, April 2000.

Abstract:

A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so far required to run an elaborate algorithm on the prefix.

Keywords:

net unfoldings, model checking, tableau systems, LTL, Petri nets

Suggested BibTeX entry:

@techreport{HUT-TCS-A60,
    address = {Espoo, Finland},
    author = {Javier Esparza and Keijo Heljanko},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {April},
    number = {60},
    pages = {32},
    title = {A New Unfolding Approach to {LTL} Model Checking},
    type = {Series A: Research Report},
    year = {2000},
}

See www.tcs.hut.fi ...

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