Distributed Places and Safe Net Reduction

TL;DR

This paper introduces a novel reduction technique for safe Petri nets using distributed places, enabling local and static simplification of systems with iterative behaviors, improving verification and implementation efficiency.

Contribution

It proposes a new concept of distributed places for safe Petri nets, allowing local reductions even in systems with iteration, enhancing previous exponential reduction methods.

Findings

Reduction is static and local, feasible in practice.

Distributed places enable deletion of places without changing behavior.

Applicable to systems with iteration, achieving polynomial size.

Abstract

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 compositionally defined safe nets. The paper discusses a novel concept of distributed place which implements 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 both static and local, making it computationally feasible in practice. The resulting reduction technique is then applied to an algebra of safe Petri nets (boxes) derived compositionally from process (box) expressions. Though the original derivation can yield exponentially large boxes, prior 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 show that similar optimisation can also be achieved in the case of process expressions with iteration.