Pre-nets, read arcs and unfolding: a functorial presentation

Pre-nets have been recently proposed as a means of providing a functorial algebraic semantics to Petri nets (possibly with read arcs), overcoming some previously unsolved subtleties of the classical model. Here we develop a functorial semantics for pre-nets following a sibling classical approach based on an unfolding construction. Any pre-net is mapped to an acyclic branching net, representing its behaviour, then to a prime event structure and finally to a finitary prime algebraic domain. Then the algebraic and unfolding view are reconciled: we exploit the algebraic semantics to define a functor from the category of pre-nets to the category of domains that is shown to be naturally isomorphic to the unfolding-based functor. All the results are extended to pre-nets with read arcs. Research supported by the FET-GC Project IST-2001-32747 Agile and by the MIUR Project COFIN 2001013518 CoMeta. The second author is also supported by an Italian cnr fellowship for research on Information Sciences and Technologies, and by the CS Department of the University of Illinois at Urbana-Champaign.