Completeness results for linear logic on petri nets

To: types@dcs.gla.ac.uk
Subject: Completeness results for linear logic on petri nets
From: Uffe Engberg <engberg@daimi.aau.dk>
Date: Mon, 22 Feb 1993 10:56:54 +0100
Approved: types@dcs.gla.ac.uk

We would like to announce the following new results:


Uffe~Henrik Engberg and Glynn Winskel.

Completeness results for linear logic on petri nets.

Submitted to MFCS'93, Gda{\'{n}}sk, Poland, August 30 - September 3,
  1993. Full version will appear as DAIMI PB, January 1993.

Abstract:

Completeness is shown for several versions of Girard's linear logic with
  respect to Petri nets as the class of models. The strongest logic considered
  is intuitionistic linear logic, with $\otimes$,
  $\mathbin{-\mkern-3mu\raise-.21ex\hbox{$\lhook\mkern-3mu\rhook$}}$,
  $\vphantom{\oplus}\raisebox{-1.15pt}{\rm\&}$, $\oplus$ and the exponential
  ${!}$ (``of course''), and forms of second-order quantification. This logic
  is shown sound and complete with respect to {\em atomic nets} (these include
  nets in which every transition leads to a nonempty multiset of places). The
  logic is remarkably expressive, enabling descriptions of the kinds of
  properties one might wish to show of nets; in particular, negative
  properties, asserting the impossibility of an assertion, can also be
  expressed.


A dvi or postscript version of the paper can be obtained by anonymous ftp from
daimi.aau.dk in the directory pub/Linear-Logic. In the same dircetory there is
a dvi and a postscript version of the CAAP'90 paper:


Uffe~Henrik Engberg and Glynn Winskel.

Petri Nets as Models of Linear Logic.

In {\em CAAP' 90, Coll.\ on Trees in Algebra and Programming
  (Copenhagen)}, pages 147--161. Springer-Verlag ({\it LNCS\/} 431), 1990.

Abstract:

The chief purpose of this paper is to appraise the feasibility of Girard's
linear logic as a specification language for parallel processes.  To this end
we propose an interpretation of linear logic in Petri nets, with respect to
which we investigate the expressive power of the logic.


Below you will find a typical ftp session.

If you have problems or questions, please do not hesitate to contact us.

	Glynn Winskel			Uffe Henrik Engberg
	Computer Science Department	Computer Science Department
	Aarhus University		Aarhus University
	Ny Munkegade			Ny Munkegade
	DK-8000 Aarhus C		DK-8000 Aarhus C
	Denmark				Denmark
	Email: gwinskel@daimi.aau.dk	Email: engberg@daimi.aau.dk


> ftp daimi.aau.dk
Connected to daimi.
220 daimi FTP server (SunOS 4.1) ready.
Name (daimi.aau.dk:engberg): anonymous
331 Guest login ok, send ident as password.
Password:
230 Guest login ok, access restrictions apply.
ftp> cd pub/Linear-Logic
250 CWD command successful.
ftp> ls
200 PORT command successful.
150 ASCII data connection for /bin/ls (130.225.16.59,1158) (0 bytes).
README
caap90.dvi.Z
caap90.ps.Z
mfcs93sub.dvi.Z
mfcs93sub.ps.Z
226 ASCII Transfer complete.
68 bytes received in 0.2 seconds (0.34 Kbytes/s)
ftp> get mfcs93sub.dvi.Z
200 PORT command successful.
150 ASCII data connection for mfcs93sub.dvi.Z (130.225.16.59,1155) (35827 bytes)
.
226 ASCII Transfer complete.
local: mfcs93sub.dvi.Z remote: mfcs93sub.dvi.Z
36010 bytes received in 0.48 seconds (73 Kbytes/s)
ftp> 221 Goodbye.
uncompress mfcs93sub.dvi.Z