A New Unfolding Approach to LTL Model Checking

Reference:

Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. Research Report A60, 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 = {A60},
    pages = {32},
    title = {A New Unfolding Approach to {LTL} Model Checking},
    type = {Research Report},
    year = {2000},
}