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

Hi Elizabeth,

I don't really know too much about model checking at all, except that I 
know that XSB Prolog have been used for it, taking advantage of the 
tabling facilities of XSB Prolog. I don't know the details of how 
tabling helps with model checking, but. ECLiPSe does not implement 
tabling, so whatever advnatage is provided by tabling would presumably 
not be provided by ECLiPSe.

I don't know enough about model checking to say if any of the libraries 
distributed with ECLiPSe will help, but in any case, these libraties 
don't support model checking and temporal logic qualifiers directly. 
There may of course be people out there who have used ECLiPSe for such 
work, but I have not heard about it.

I just did a littel checking on the net, and apparently there are some 
work done with CLP and model checking. I know nothing about this, but I 
assume you probably already know about these work, and know if the 
constraint libraries provided by ECLiPSe are suitable for your needs or 
not.

Cheers,

Kish

Elizabeth Barham wrote:
> 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
>
> _______________________________________________
> ECLiPSe-Users mailing list
> ECLiPSe-Users_at_crosscoreop.com
> http://www.crosscoreop.com/mailman/options/eclipse-users
>