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 kr…@ira.uka.de
Thomas Kropf
Institute of Computer Design and Fault Tolerance
University of Karlsruhe
West-Germany
In article <9…@iraun1.ira.uka.de> kr…@i81s1.ira.uka.de () writes:
>I am looking desperately for theorem provers which are able to cope with
>temporal logic, especially with linear temporal logic
You might be interested in Moszkowski’s book "Executing Temporal Logic
Programs," (Cambridge 1986). See its review in The Journal of Symbolic
Logic, LIII 309, and the references given there to related work.
In article <9…@iraun1.ira.uka.de> kr…@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 (j…@CAT.CMU.EDU)
In article <1…@sunset.MATH.UCLA.EDU> h…@math.ucla.edu (H. Enderton) writes:
>In article <9…@iraun1.ira.uka.de> kr…@i81s1.ira.uka.de () writes:
>>I am looking desperately for theorem provers which are able to cope with
>>temporal logic, especially with linear temporal logic
>You might be interested in Moszkowski’s book "Executing Temporal Logic
>Programs," (Cambridge 1986). See its review in The Journal of Symbolic
>Logic, LIII 309, and the references given there to related work.
Another person worth trying is Prof. Dov Gabbay at Imperial College London,
he is working with somebody at Manchester University (whose name I forget for
the moment) on executing temporal sepecifications.
A. Mahmood
Laboratory for Foundations of Computer Science
Edinburgh University
Scotland
Ben Moskowski has a language ITL and an executable subset Tempura for
programming using a version of interval temporal logic. see his book
`Executing Temporal Logic Specifications’, Cambridge UP 1986. Also
Roger Hale’s article in Galton’s book `Temporal Logics and Their
Applications’ Wiley 1987. In Galton’s book also is an article by
Gabbay which extends Horn Clause Theorem Proving to temporal logics,
and there is a comment in there attributed to Kowalski showing how
the behaviour of the prover may be emulated by an ordinary Prolog
interpreter. Luis Farin~as del Cerro has been working in theorem
provers for modal logics for some time – see his article in the
CADE Proceedings (Napa 1984, I don’t remember which CADE this is).
I’m sure there are some more recent articles of his also. Martin
Abadi has also designed a resolution principle for temporal logics,
and has many papers. I’m not sure of the best reference.
He’s at decsrc.dec.com. Michael McRobbie is editing a special issue
of the Journal of Automated Reasoning on Non-Standard Logics, including
temporal ones, so he is probably able to give excellent pointers.
He’s at the Australian National University, anu.oz.
I’m sure I’ve left obvious references out – this is off the top of my head,
so apologies to those unmentioned.
peter ladkin
Ed Clarke at Carnegie Mellon has some nice programs for doing this
I believe.
Peter Ladkin’s list covered nearly everything I’ve ever heard of. One other
is the Temporal Prolog designed by Takashi Sakuragawa of the Research Institute
of Mathematical Sciences at Kyoto University; but my only reference for this is
a technical report, and I don’t know if it was ever published or how far his
implementation got.