Monotonicity Properties in Petri Nets

Petri nets follow two important principles of monotonicity that describe how their behavior remains consistent when initial conditions change. Understanding these properties helps explain why Petri nets are such a powerful model for analyzing dynamic systems and concurrent processes.

Property 1

If a transition sequence σ can be fired from two different initial markings M'0[σ>M' and M''0[σ>M'', then after firing the sequence, the difference between the markings stays the same: $$ M'_0 - M' = M''_0 - M'' $$ $$ M'_0 - M''_0 = M' - M'' $$

Explanation

This property comes directly from the state equations that describe how the markings evolve during transitions:

$$ M' = M'_0 + C \cdot σ $$

$$ M'' = M''_0 + C \cdot σ $$

Subtracting the second equation from the first, we find:

$$ M' - M'' = M'_0 + C \cdot σ - (M''_0 + C \cdot σ) $$

which simplifies to:

$$ M' - M'' = M'_0 - M''_0 $$

This shows that the relative difference between markings remains constant throughout the transition sequence, regardless of the initial state.

Property 2

If one marking M'0 contains at least as many tokens as another marking M''0 (that is, M'0 ≥ M''0), then every transition sequence enabled from M''0 is also enabled from M'0: $$ L(N, M''_0) \supseteq L(N, M'_0) $$

Here, L represents the set of all transition sequences (the “language”) that can be executed starting from a given marking.

Explanation

Let’s consider a sequence of transitions:

$$ σ = t_1 t_2 ... t_j $$

Each transition updates the marking, starting from M''0:

$$ M''_0[t_1>M''_1[t_2>...[t_j>M''_j $$

Since

$$ M'_0 \ge M''_0 \ge Pre(*, t_j) $$

we can conclude that the same transition is also enabled from M'0:

$$ M'_0[t_1> M'_1 = M'_0 - M''_0 + M''_1 \ge M''_1 $$

and this reasoning holds for every subsequent transition in the sequence.

In essence, having more tokens (a “larger” marking) can only enable more behavior, never less. This makes Petri nets particularly useful for reasoning about system growth, scalability, and the preservation of logical consistency across different states.

 


 

Segnalami un errore, un refuso o un suggerimento per migliorare gli appunti

FacebookTwitterLinkedinLinkedin
knowledge base

Petri Net