Distributed Places and Safe Net Reduction

TL;DR

The paper addresses synthesising compact, behaviourally equivalent safe Petri nets from compositional specifications expressed as box expressions. It introduces distributed places as locally defined, monotone state-ful units and proves a static, local reduction that preserves reachability semantics. By coupling these ideas with box-algebra translations and a cograph-based approach, it shows how to obtain polynomial-size reductions via edge clique covers, even for iterative constructs. The methods combine structural decomposition (distributed places, cross-product) with graph-theoretic reductions (cographs, eccp peccp) to enable scalable synthesis of reduced nets that preserve behaviour, offering practical routes for verification and implementation of concurrent systems.

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.

Figures (7)

• Figure 1: ($a$) A net translated from box expression $[ {a\,{\Box}\, b} *{c\,{;}\,(d\,{\|}\, e)}*{f\,{\|}\, g}]$. ($b$) A net expressing choice between three pairs of concurrent actions, $a_i$ and $b_i$, and ($c$) its reduced version exhibiting the same behaviour. ($d$) A reduced version of a marked net expressing choice between 10 pairs of concurrent actions, $a_i$ and $b_i$.
• Figure 2: ($a$) A safe Petri net $\mathcal{N}_0$, ($b$) its reduced behaviourally equivalent net $\mathcal{N}'_0$, and ($c$) a sequential component $\mathcal{S}_i$ of $\mathcal{N}_0$ ($i=3,4,\dots,10$).
• Figure 3: ($a,b,c$) Three distributed places, $\mathcal{P}$, $\mathcal{P}'$, and $\mathcal{P}"$, together with surrounding transitions for the marked nets in Figure \ref{['fi-1']}($a,b)$. ($d$) A set of places $Q=\{p_6,p_7,p_{10}\}$ with surrounding transitions which is not a distributed place for the marked net $\mathcal{N}_0$ in Figure \ref{['fi-1']}($a$).
• Figure 4: ($a$) A net $\mathcal{N}_1=\mathop{\mathrm{box}}\nolimits((a\,{\|}\, b)\,{;}\,(c\,{\|}\, d))$, and ($b$) its unsuccessful reduction $\mathcal{N}'_1$. ($c$) A net $\mathcal{N}_2=\mathop{\mathrm{box}}\nolimits((a\,{\|}\, b)\,{\Box}\,(c\,{\|}\, d))$, and ($d$) its unsuccessful reduction $\mathcal{N}'_2$.
• Figure 5: ($a$) A net $\mathcal{N}_3=\mathop{\mathrm{box}}\nolimits((a\,{\|}\, b);((c\,{\|}\, d)\,{\Box}\,(e\,{\|}\, f)))$, and ($b$) its reduced version $\mathcal{N}_3'$.

Theorems & Definitions (28)

• Example 2.1
• Definition 3.1: in-sequence and out-sequence
• Definition 3.2: distributed place
• Example 3.3
• Proposition 3.4
• Proposition 3.5
• Theorem 3.6
• Corollary 3.7
• Theorem 3.8
• Proposition 4.1