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)