Research Report A60: A New Unfolding Approach to LTL Model Checking

Author: Javier Esparza and Keijo Heljanko

Date: April 2000

Pages: 32

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

Full report in Postscript