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, 30 Mar 1995 13:01:51 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA235873406;
          Thu, 30 Mar 1995 04:36:46 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from eagle.eng.warwick.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA235843403;
          Thu, 30 Mar 1995 04:36:43 -0700
Received: from eng.warwick.ac.uk by eagle.eng.warwick.ac.uk with SMTP 
          id MAA23454; Thu, 30 Mar 1995 12:33:50 +0100
From: es2033@eng.warwick.ac.uk
Message-Id: <7611.9503301133@eng.warwick.ac.uk>
Subject: Timed CSP in HOL?
To: info-hol@leopard.cs.byu.edu
Date: Thu, 30 Mar 95 12:33:49 BST
X-Mailer: ELM [version 2.3 PL8]


   Hi,

   I am trying to use Timed CSP to specify real-time software requirements.
   Has anyone constructed a theory of "timed CSP" in HOL(HOL88) ?
   (I know that there is untimed CSP by A. Camilleri in contrib directory.)
   
   Thanks.

   N. Hur -- email : es2033@eng.warwick.ac.uk