Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <8155.9410120940@frogland.inmos.co.uk>
Subject: Re: "Re: Single Pulser"
To: schneide@ira.uka.de (schneide)
Date: Wed, 12 Oct 1994 10:40:15 +0100 (BST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <"i80fs2.ira.475:12.10.94.09.20.34"@ira.uka.de> from "schneide" at Oct 12, 94 10:20:31 am
Content-Type: text
Content-Length: 2485

schneide has said:
> David Shepherd said:
> 
> |> I claim that this spec is way over the top in complexity - ? was it
> |> autogenerated from some tool that builds recogniser automata from
> |> another logic (e.g. there's a program that produces SMV modules to
> |> recognise LTL specs).
> 
> I agree. There are certainly lots of states which are unnecessary. 
> Actually, there is no tool which generates this output, but I am currently
> implementing such a tool. The transformation in a SMV-description 
> similar to the one I gave, can be done completely safe (i.e. without
> mk_thm) in HOL. The output will then be exactly what I have 
> generated by hand.

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.

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?

> Even if it is possible in this example to give a straightforward spec
> directly in CLT, I do not believe that this is as simple for other
> specifications as well. This is because the branching time has some
> effects which seem to be unnatural to me, e.g. the NEXT operator
> can be distributed over all other operators in linear logic, but not
> in CTL, i.e. NOT(NEXT x) is not NEXT(NOT x) does hold in linear
> logic.
>
> So, are people able to think in CTL directly? I am not sure about that.
> 
> The tool does therefore also translate linear logic into branching
> time logic.

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.

One thing that struck me when I was at this years CAV meeting, which
is very much orientated towards automated model checking, was how
much attention every paid to complexity bounds of algorithms. I
forget the exact details but CTL is significantly less complex than
LTL which is in turn less complex than CTL*.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."