Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <199410131601.MAA07324@air55.larc.nasa.gov>
Date: Thu, 13 Oct 1994 12:01:24 -0400
From: "Paul S. Miner" <psm@air16.larc.nasa.gov>
To: info-hol@cs.uidaho.edu
Subject: [sjohnson@cs.indiana.edu: Could one of you post this to the HOL 
         newsgroup.]

Return-Path: <sjohnson@cs.indiana.edu>
From: "steve johnson" <sjohnson@cs.indiana.edu>
Subject: Could one of you post this to the HOL newsgroup.
To: zhu@cs.indiana.edu (zheng zhu), psm@cs.indiana.edu
Date: Wed, 12 Oct 1994 16:09:11 -0500 (EST)
X-Mailer: ELM [version 2.4 PL21]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 2521      

Paul or Zheng.

Thanks for the transcripts; Kathi has also told me about them.  I'm just
back from ICCD and catching up on my mail so I haven't had much time
to study the correspondence among members of the HOL group.  However,
from my first impression, the discussion of CTL may not be a reflection
of what actually occurred at the meeting.  Would you please post this
note with my promise to follow up with a more detailed discussion.

It is true that we had substantial difficulty representing in CTL
the facts which we wanted to prove about the single pulser.  Indeed, the
attempt that appears in the participants' proceedings is not only
cumbersome, but may also be incorrect, and further, is an overly strong
proposition.

We (the listed coauthors) are very indebted to Albert Camerelli who
looked at the section at the TPCD workshop and made some suggestions.
On our return from Bad Herrenalb, Kathi Fisler and I worked with the
formulas suggested by Albert. They are certainly more elegant, almost
certainly correct, and they have been accepted as true by SMV.

I want to look very carefully at the solution before publishing it
and that will take a couple of days.  In the mean time, I would like
to clarify:  Most important, we were able to specify the properties of interest
about the single pulser in CTL.  Our first attempt was not very elegant---and
I am told that we made the kinds of stylistic mistakes that are common when
people first use the logic.  But nevertheless, the properties of interest
were expressible in CTL.

Second, I want to acknowledge that one of our goals in this series of studies
is to approach each system with a kind of freshness, or innocence of mind, that
might allow us to explain to someone not versed in verification methodogy
what some of the basic intellectual "startup" problems are in each tool and
logic.  We may have been succeeded beyond our dreams with CTL,
but our general impression has been that  e a c h  formalism exacts its own
kind of intellectual toll and that, over all, these appear to be
quite comparable.

I am very happy to see people taking an interest in this set of studies and
I hope that more can be initiated.  We will continue to maintain the
single pulser examples in cooperation with IFIP WG 10.5 (formerly 10.2).

More later...

Steve Johnson______________________________________________
Computer Science Department   net: sjohnson@cs.indiana.edu
Indiana University            tel: 812-855-2567
Bloomington, IN 47405-4101    fax: 812-855-4829