Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 12 Oct 1994 10:26:00 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA00848; Wed, 12 Oct 1994 03:24:09 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA00844; Wed, 12 Oct 1994 03:24:07 -0600 Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id CAA18246 for ; Wed, 12 Oct 1994 02:17:24 -0700 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Wed, 12 Oct 1994 10:17:05 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <01473-0@i80fs2.ira.uka.de>; Wed, 12 Oct 1994 10:20:32 +0100 To: info-hol@cs.uidaho.edu Subject: "Re: Single Pulser" Date: Wed, 12 Oct 1994 10:20:31 +0100 From: schneide Message-Id: <"i80fs2.ira.475:12.10.94.09.20.34"@ira.uka.de> 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. 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. Klaus.