Xref: utzoo sci.logic:467 comp.ai:4414 comp.lang.lisp:1925 comp.lang.prolog:1799
Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!tut.cis.ohio-state.edu!pt.cs.cmu.edu!cat.cmu.edu!jps
From: jps@cat.cmu.edu (James Salsman)
Newsgroups: sci.logic,comp.ai,comp.lang.lisp,comp.lang.prolog
Subject: Re: Theorem Provers for Temporal Logic
Message-ID: <5452@pt.cs.cmu.edu>
Date: 10 Jul 89 01:41:02 GMT
References: <928@iraun1.ira.uka.de>
Organization: Carnegie Mellon
Lines: 22

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)