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; Thu, 13 Oct 1994 17:59:10 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA21661;
          Thu, 13 Oct 1994 10:57:27 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA21657;
          Thu, 13 Oct 1994 10:57:27 -0600
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA14614;
          Thu, 13 Oct 1994 10:52:07 -0600
Message-Id: <9410131652.AA14614@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Forward of message from David Fura (another CTL teaser)
Date: Thu, 13 Oct 1994 10:52:06 -0600
From: Phil Windley <windley@lal.cs.byu.edu>


------- Forwarded Message

Date: Wed, 12 Oct 94 23:37:55 PDT
From: dfura@elvis.ds.boeing.com (David Fura)
Message-Id: <9410130637.AA17474@elvis.ds.boeing.com>
To: info-hol@cs.uidaho.edu
Subject: another CTL teaser

Since we're already on the subject ...

I've been playing around with CTL as well and haven't yet
been able to find a representation for the following:

"if rqt is high 
 then it will go low on the next cycle and remain low 
      while ack has been high fewer than 2 times (since rqt was high)"

Here, "while" is similar to "weak until" so that another
way to say the same thing is:

"if rqt is high
 then it will go low on the next cycle and remain low 
      until (weak) ack is high at least 2 times (since rqt was high)" 

I've presented this to 2 people I would consider experts in CTL
and got: (i) a wrong answer and (ii) a list of reference papers.
It's my *opinion* that this cannot be represented in CTL (or LTL)
but wouldn't mind a counterexample.

 -- Dave

------- End of Forwarded Message