A Linear Specification Language for Petri Nets

Authors:
Open Access
Publisher website
Google Scholar
Abstract
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.

This publication has 3 references indexed in Scilit: