Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 11 May 1994 10:51:29 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17266;
          Wed, 11 May 1994 03:34:00 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA17261;
          Wed, 11 May 1994 03:32:08 -0600
Received: from irafs1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA11308;
          Wed, 11 May 1994 02:32:42 -0700
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Wed, 11 May 1994 11:26:14 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <23925-0@i80fs2.ira.uka.de>;
          Wed, 11 May 1994 11:32:01 +0200
To: info-hol@cs.uidaho.edu
Subject: Proving LTL with ARITH_CONV
Date: Wed, 11 May 1994 11:32:00 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.929:11.04.94.09.32.08"@ira.uka.de>

Hi all,

Linear temporal logic is very important for the verification of digital
circuits or other concurrent systems. For this reason, some people 
developed theories in HOL which are based mainly on this logic.
However, there is no efficient decision procedure for this logic
in HOL (as far as I know). However, there are strong relations between 
linear temporal logic and pressburger arithmetic. To motivate this look 
at the following two facts:

   (i) Each predicate which is definable in pressburger arithmetic
       is ultimatively periodic (i.e. there are numbers x0 and l such 
       that (0<l) /\ !t.P(x0+t) = P(x0+((t-x0)MOD l)) holds). A proof
       can be found in the book of Enderton.

  (ii) Models of a linear temporal logic formula are also ultimatively
       periodic, since they can be accepted by automata for omega
       regular languages. A proof of this fact is due to Vardi, Wolper
       and Sistla (as far as I know).

Now the question:
Has anyone ever thought of using ARITH_CONV for proving temporal logic
formulae?


Klaus.