Xref: utzoo comp.theory:1240 sci.logic:1035
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!mintaka!bloom-beacon!eru!hagbard!sunic!news.funet.fi!hydra!hylka!rkaivola
From: rkaivola@cc.helsinki.fi
Newsgroups: comp.theory,sci.logic
Subject: A request for temporal logic tools
Message-ID: <4054.274aa972@cc.helsinki.fi>
Date: 21 Nov 90 16:21:05 GMT
Organization: University of Helsinki
Lines: 35



Sorry if this is a duplicate, but the original posting did not seem to
make is beyond the local node.


We are currently looking for automated tools for temporal logics,
in particular for the temporal logics of programs. 
As far as we know there exist references in the literature to tools 
belonging to the following categories:

* temporal logic programming languages (e.g. TEMPURA, TEMPLOG, TOKIO ) 

* temporal logic theorem provers (e.g. resolution methods, tableau methods,
  automata theoretic methods, proof editors)

* temporal logic model checkers (e.g. for CTL, FCTL, linear time logic and
  full branching time logic)

If you can supply us with any information concerning the existence and
availability of such tools (from whom to order, approximate costs etc.) 
or your own experiences in using these tools in practice, your contribution 
will be gratefully received. Should your contribution not fall in the 
aforementioned categories please do not let this deter you from submitting.

If there will be enough interest, we will summarise for the net.


Roope Kaivola

rkaivola@cc.Helsinki.fi                 University of Helsinki
rkaivola@finuh.EARN                     Department of Computer Science
                                        Teollisuuskatu 23
                                        SF-00510 Helsinki
                                        Finland