We report on an implementation of the unfolding approach to model-checking LTL-X recently presented by the authors. Contrary
to that work, 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 efficiently. We present results on a set of case studies.
Work partially supported by the Teilprojekt A3 SAM of the Sonderforschungsbereich 342 “Werkzeuge und Methoden für die Nutzung
paralleler Rechnerarchitekturen“, the Academy of Finland (Projects 47754 and 43963), and the Emil Aaltonen Foundation.