Article View: sci.logic
Article #81Re: Theorem Provers for Temporal Logic
From: James Salsman
Date: Mon, 10 Jul 1989 01:41
Date: Mon, 10 Jul 1989 01:41
22 lines
1292 bytes
1292 bytes
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)
Technical Details
Message-ID:
<5452@pt.cs.cmu.edu>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!tut.cis.ohio-state.edu!pt.cs.cmu.edu!cat.cmu.edu!jpsReferences:
<928@iraun1.ira.uka.de>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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