[sci.logic] Theorem Provers for Temporal Logic

kropf@i81s1.ira.uka.de (07/07/89)

Working in the fields of hardware specification and verification,
I am looking desperately for theorem provers which are able to cope with
temporal logic, especially with linear temporal logic 
(as proposed e.g. by Manna & Pnueli).

Every reference to available systems or to people coping with 
such tools are gratefully appreciated!

Please E-mail (CS-Net) to kropf@ira.uka.de

Thomas Kropf
Institute of Computer Design and Fault Tolerance
University of Karlsruhe
West-Germany 

jps@cat.cmu.edu (James Salsman) (07/10/89)

In article <928@iraun1.ira.uka.de> kropf@i81s1.ira.uka.de () writes:
> Working in the fields of hardware specification and verification,
> I am looking desperately for theorem provers which are able to cope with
> temporal logic, especially with linear temporal logic 
> (as proposed e.g. by Manna & Pnueli).

Good question...  Although I'm not familiar with Manna &
Pnueli's work, I suggest that you look into Bayesian and
Marcov-Model based logics -- the idea of predication is best
expressed in terms of fuzzy set and probability theory.

The disadvantage is that to construct a Marcov model you
need a large training set of "historical" data.  Can you
collect that data?  If not, construct a few "specifications"
and "verifications" yourself and use that as a basis.  Then
tune your model when it gets older.

:James
::chgrp
-- 

:James P. Salsman (jps@CAT.CMU.EDU)