A Linear Specification Language for Petri Nets

This paper defines a category GNet with object set all Petri nets. A morphism in GNet from a net N to a net N' gives a precise way of simulating every evolution of N by an evolution of N'. We exhibit a morphism from a simple message handler to one with error-correction, showing that the more refined message handler can simulate any behaviour of its simple counterpart. The existence of such a morphism proves the correctness of the refinement