Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu
Subject: LTL Proving by ARITH_CONV
Date: Tue, 31 May 1994 09:46:09 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.649:31.04.94.07.46.12"@ira.uka.de>

Geoffrey Hird wrote:

|>   The way to look at the relationship is as follows.  Both Presburger
|> arithmetic and linear temporal logic can easily be interpreted in S1S
|> (the monadic second order theory of one successor).  S1S was shown
|> decidable by Buechi, and formulas of this theory define ultimately
|> periodic sets of \omega.

I agree to all of that, indeed the paper I presented at the last HOL
workshop considered `hardware formulae' which is a subclass of
Buechi's Buechiformulae (which I consider now, too).
 
|>  The decision procedure in ARITH_CONV, last time I used HOL (2 years
|> ago) was at most quantifier-free Presburger arithmetic, as I recall
|> (but I'm not sure), and I would be surprised if it were the full
|> theory now.

 However, there are also relations to weaker formalisms. Kamp has
proved that linear temporal (propositional) logic is equivalent
to the first order theory of linear order, and this is again a fragment
of pressburger arithmetic. 

|> So it may be easy to get the correspondence
|> you want (noting that one bunch of universal quantifiers is the same
|> as quantifier-free with free variables).  I haven't any time to look
|> at it right now -- it should be either obviously do-able or obviously
|> hard.

I suppose, that a translation into the first order theory of linear order
is quite trivial. I did some of these translations in implementing
temporal operators. I implemented the operators ALWAYS, EVENTUAL,
UNTIL, WHEN, BEFORE and WHILE, but I list just theorems for WHEN.


The definition of WHEN was given as hardwareformula:

  WHEN
    |- !x b t0.
         (x WHEN b) t0 =
         (?q.
           (!t. (q t0 = F) /\ (q (SUC (t + t0)) = q (t + t0) \/ b (t + t0))) /\ 
           (!t. q (t + t0) \/ (b (t + t0) ==> x (t + t0))))

Then one can prove a recursion theorem
    WHEN_REC |- (x WHEN b) t0 = ((b t0) => (x t0) | (NEXT (x WHEN b) t0))

and the relation to arithmetic:
  WHILE_SIGNAL
    |- (x WHILE b) t0 =
       ((!t. b (t + t0)) ==> (!t. x (t + t0))) /\
       (!d.
         (!t. t < d ==> b (t + t0)) /\ ~(b (d + t0)) ==>
         (!t. t < d ==> x (t + t0)))

Additionaly, I proved invariant theorems for making proofs in temporal
first and higher order logic:

  WHEN_INVARIANT_THM
    |- (x WHEN b) t0 =
       (?J.
         J t0 /\
         (!t. ~(b (t + t0)) /\ J (t + t0) ==> J (SUC (t + t0))) /\
         (!d. b (d + t0) /\ J (d + t0) ==> x (d + t0)))

I implemented a complete theory of all these temporal operators, but
at the moment I have no decision procedure in HOL. Instead I translate
temporal terms into Buechi automata (this is done formally in HOL)
and give the resulting goals to an external model checker (SMV).

Maybe, the translation to pressburger arithmetic can be done
reasonably efficiently. Otherwise, it would be interesting to 
implement a decision procedure not only for pressburger, but
for the entire S1S.


Maybe I can report at the HUG95 about that,
 Klaus.