11 Dec 1990 16:50
A little linear logic observation about Petri Nets
Date: Tue, 11 Dec 90 13:57:43 GMT A little linear logic observation about Petri Nets Carolyn Brown (from Edinburgh) was here (Imperial College, London) last week talking about her categories of Petri nets based on Valeria de Paiva's "dialectica categories" (Carolyn presented her work at LiCS this year). Afterwards, Carolyn and I tried but failed to make sense of an idea of mine that Petri nets were "internal categories" in some context in which Valeria's construction provided the "sets". However we did come up with a cute little formula for sequences of actions which has a linear logic interpretation. For those who are confused by the many different understandings of linear logic in Petri Nets, let me just point out that what follows depends only on the "trivial" observation that markings are additive, whereas Valeria & Carolyn's work involves amuch more suble tensor. I have in mind Petri nets which * at first require at most one token from each place for an event, * in the second case require an arbitrary natural number of them, * and in the general case the input (and similarly the output) is an element of a complete ordered monoid, or even a monoidal category. First I'll phrase my argument in the "natural numbers" case. I want to find the pre- and postconditions of the sequence $e;f$ in terms of those of the events $e$ and $f$. For each place $b\in B$, clearly we need at least $pre(e,b)$, else we couldn't perform $e$. Then we need no more if $post(e,b)\geq pre(f,b)$, but otherwise $pre(f,b)-post(e,b)$ in addition. Likewise the output is at least $post(f,b)$, but there may be a left-over $post(e,b)-pre(f,b)$ in addition if this is nonnegative.(Continue reading)
RSS Feed