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 ·····@ira.uka.de
Thomas Kropf
Institute of Computer Design and Fault Tolerance
University of Karlsruhe
West-Germany
From: James Salsman
Subject: Re: Theorem Provers for Temporal Logic
Date:
Message-ID: <5452@pt.cs.cmu.edu>
In article <···@iraun1.ira.uka.de> ·····@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 (···@CAT.CMU.EDU)