Distributed Places and Safe Net Reduction

Being able to find small Petri nets with the same behaviour as formal specifications of concurrent systems benefits both effective verification and practical implementation of such systems. This paper considers specifications given in the form of safe nets and process expressions.The paper introduces a novel concept of ‘distributed place’ which abstracts the behaviour of an individual net place. It is shown that if distributed places cover a safe Petri net, then it is possible to delete some places without changing the behaviour. Crucially, the reduction is carried out both statically and locally, making it computationally feasible in practice.The resulting reduction technique is then considered for an algebra of safe Petri nets (boxes) derived from process (box) expressions. Though the original derivation can yield exponentially large boxes, the recent research demonstrated that if a box expression does not involve cyclic behaviours, the exponential number of places can be reduced down to polynomial (quadratic). In this paper, using distributed places, it is demonstrated that similar optimisation can also be achieved in the cyclic case.