Le proprietà di monotonia della rete di Petri
Una rete di Petri soddisfa due proprietà di monotonia.
Proprietà 1
Se una sequenza di transizione σ è abilitata da due marcature M'0[σ>M' e M''0[σ>M'', dopo lo scatto la differenza è la stessa $$ M'_0-M' = M_0'' - M'' $$ $$ M'_0-M''_0 = M' - M'' $$
Dimostrazione
Le equazioni di stato delle marcature sono
$$ M'=M'_0+C \cdot σ $$
$$ M''=M''_0+C \cdot σ $$
Sottraggo membro a membro la seconda equazione nella prima
$$ M'-M''=M'_0+C \cdot σ -M''_0+C \cdot σ $$
$$ M'-M''=M'_0 -M''_0 $$
$$ M'_0-M' = M_0'' - M'' $$
oppure
$$ M'_0-M''_0 = M' - M'' $$
Proprietà 2
Se una marcatura M'0≥M''0 allora ogni sequenza abilitata da M''0 è anche abilitata da M'0 $$ L(N,M''_0) \supseteq L(N,M'_0) $$
Dove L è il linguaggio della marcatura.
Dimostrazione
Una sequenza di transizioni abilitata è
$$ σ=t_1 t_2 ... t_j $$
Le transizioni modificano le marcature a partire da M''0
$$ M''_0[t_1>M''_1[t_2>...[t_j>M''_j $$
Poiché
$$ M'_0 ≥ M''_0 ≥ Pre(*,t_j) $$
allora
$$ M'_0[t_1> M'_1 = M'_0-M''_0+M''_1 \ge M''_1 $$
E così via.
