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: Re: Single Pulser
Date: Wed, 12 Oct 1994 11:16:23 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.881:12.10.94.10.16.29"@ira.uka.de>

I have to apologize to use info-hol for a LTL-CTL discussion, but
both LTL and CTL are interesting formalisms which could/should be
implemented in HOL/HOL2000. I have already a theory of temporal
linear time operators which I can make available. But I know, that
some more people do also have such theories.


Again, D. Shepherd has said:
|> What I was disputing was the claim that the property couldn't be 
|> described in CTL and needed all extra stuff in the main module to
|> capture the spec.

Yes, of course you can express these things directly in CTL. However,
I am concerned about the understanding of nested branching time
operators. The spec you gave only uses A-Operators, but if you have
mixtures with E-Operators things can become quickly awkward.

|> BTW, I'm not sure exactly what your tool is ... is it a proof system
|> for such SMV like machines in HOL or is it a method of generating an
|> equivalent CTL formula from a more general one?

My (future) tool is translating a fragment (which I however can not formalize here)
of LTL into automata-like formulae in HOL. This translation is however
not done as in the mentioned CAV94 paper (which required exponential time
in the worst case). Instead, it uses some facts of the properties of the 
fragment and therefore the translation can be done in linear time.
Of course, not everything can be expressed in this fragment, e.g. 
fairness is lost. However, from the hardware specification point of
view I am surprised how many specifications fall into this fragment.

|> Certainly, from brief experimentation with a LTL->CTL translator
|> someone at CMU has done (see CAV94 for details), LTL is certainly
|> much more "natural" to think about - however, if you can express
|> something in CTL then it is about 2 or 3 times more efficient than
|> doing the same in translated LTL.

Yes, LTL model checking is no more polynomial and as complex as 
LTL satisfiability checking. However, often the fact is mentioned
that CTL model checking can be done in linear time (in terms of
the length of the formulae and the size of the model), but I heard
somewhere that LTL is exponentially more succint than CTL, i.e.
there are facts which can be expressed with relatively small
LTL-formulae, but only with large CTL formulae. So, at the end,
the complexity is all the same, if you consider the same problem.


Klaus.