In: Nielsen, M.; Simpson, D.: Lecture Notes in Computer Science, Vol. 1825: 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), Aarhus, Denmark, June 2000, pages 123-145. Springer-Verlag, 2000.
Abstract: In this paper, we present new technique designing to solve the on-the-fly model checking problem for linear temporal logic using unfolding graphs. Our study is based on the recognition of stuttering behavior in a formula automaton and on the on-the-fly construction of an unfolding graph. Moreover, the characterization of different kinds of behaviors allows us to design efficient algorithms for the detection of accepting paths. We have extended our study to the use of the atomic proposition dead which holds for terminal states. Partial order techniques are not adapted to deal with this global property in the context of a LTL model checking.