Return-Path: Delivery-Date: Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 13 Dec 1995 13:33:23 +0000 Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk with esmtp (Exim 0.24 #26) id E0tPrIz-0003X2-00; Wed, 13 Dec 1995 13:33:10 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA149339267; Wed, 13 Dec 1995 05:54:27 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA149309265; Wed, 13 Dec 1995 05:54:25 -0700 Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with SMTP id EAA09755 for ; Wed, 13 Dec 1995 04:54:07 -0800 Received: from ira.uka.de (actually i80s35.ira.uka.de) by iraun1.ira.uka.de with SMTP (PP); Thu, 7 Dec 1995 18:54:32 +0100 X-Mailer: exmh version 1.5.3 12/28/94 To: info-hol@cs.uidaho.edu Subject: Theory of Temporal Operators Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Thu, 07 Dec 1995 18:53:37 +0100 From: schneide Message-Id: <"iraun1.ira.910:07.12.95.17.54.33"@ira.uka.de> I implemented a HOL theory of linear temporal Operators which formalizes linear temporal logic in HOL. The theory defines the temporal operators ALWAYS, EVENTUAL, WHEN, UNTIL, BEFORE, SWHEN, SUNTIL and SBEFORE. A lot of theorems are proven about these operators which cover also the characterisation of the linear time operators by finite omega automata, fixpoint calculi and monadic successor arithmetic. Furthermore, some theorems have been proved which allow to translate linear temporal logic into omega automata. Tools for this translation will be available in the near future. If you are interested in the theory, you can obtain a gziped tar-file frome my Web-Homepage under the following URL: http://goethe.ira.uka.de/people/schneider/schneider.html Klaus.