[eclipse-users] temporal logic libraries? model checking recs?

Hi,

Are there any libraries for ECLiPSe that facilitate model checking
and/or the use of temporal logic qualifiers? If not, does anyone know
of any documents about using ECLiPSe for these purposes? I'm working
on a paper tentatively entitled "Model Checking with CLP" and am
hoping to end the paper with an example using ECLiPSe as the CLP
platform.

Thank you,
Elizabeth