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