Implementing LTL model checking with net unfoldings
Javier Esparza, Keijo Heljanko · 2001
Abstract We report on an implementation of the unfolding approach to model-checking LTL-X presented in [3]. Contrary to [3], we consider an state-based version of LTL-X, which is more used in practice. We improve on the checking algorithm; the new version allows to reuse code much more eciently. We present results on a set of case studies. 1