We present a novel method for proving temporal properties of the behaviour a Petri net. Unlike existing methods, which involve an exhaustive examination of the transition system representing all behaviours of the net, our approach uses morphisms dependent only on the static structure of the net. These morphisms correspond to refinements. We restrict the analysis of dynamic behaviours to particularly simple nets (test nets), and establish temporal properties of a complex net by considering morphisms between it and various test nets. This approach is computationally efficient, and the construction of test nets is facilitated by the graphical representation of nets. The use of category theory permits a natural modular approach to proving properties of nets.
Our main result is the syntactic characterisation of two expressive classes of formulae: those whose satisfaction is preserved by morphisms and those whose satisfaction is reflected.