Place/transition (PT) Petri nets are one of the most widely
used models of concurrency.
However, they still lack, in our view, a satisfactory semantics: on the
one
hand the ‘token
game’ is too intensional, even in its more abstract interpretations
in terms of nonsequential
processes and monoidal categories; on the other hand, Winskel's basic
unfolding
construction, which provides a coreflection between nets and finitary prime
algebraic
domains, works only for safe nets. In this paper we extend Winskel's
result to PT nets. We
start with a rather general category PTNets of PT nets, we introduce a
category DecOcc of
decorated (nondeterministic) occurrence nets and we define adjunctions
between PTNets and
DecOcc and between DecOcc and Occ, the category of occurrence nets.
The role of DecOcc
is to provide natural unfoldings for PT nets, i.e., acyclic safe nets
where a notion of family is
used to relate multiple instances of the same place. The unfolding
functor from PTNets to
Occ reduces to Winskel's when restricted to safe nets. Moreover,
the standard coreflection
between Occ and Dom, the category of finitary prime algebraic domains,
when composed
with the unfolding functor above, determines a chain of adjunctions
between PTNets and Dom.
Correction to: Transactions on Petri Nets and Other Models of Concurrency XV