Modelsof DistributedSystems [629491]

Modelsof DistributedSystems
Lecture4
MSD (2020) Lecture4 1/ 41

Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 2/ 41

LinearAlgebraicTechniques Place Invariants
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 3/ 41

LinearAlgebraicTechniques Place Invariants
Place Invariants
Definition 1
Let N= (P,T,F,W)a markedPetrinet . N iscovered byP-invariantsiff thereexistsa
P-invarianti such that ||i||=P.
MSD (2020) Lecture4 4/ 41

LinearAlgebraicTechniques Place Invariants
Place Invariants
Definition 1
Let N= (P,T,F,W)a markedPetrinet . N iscovered byP-invariantsiff thereexistsa
P-invarianti such that ||i||=P.
p1 t2t3t1
p3p2
2(x,y,z)·
1 1 0
0−1 1
0 1 −1
=0=⇒
P-invariants: (0,α,α)
Thenet is notcovered byP-invariants(theredoesnot exists a P-invarian ti>0withi(p1)/ne}ationslash=0)
MSD (2020) Lecture4 4/ 41

LinearAlgebraicTechniques Place Invariants
Place Invariants
Theorem1
Letγ= (N,M0)bea marked Petrinet .
(1)If i>0isa P-invariantof N, thenanyplace p ∈ ||i||isbounded.
(2)Ifγis coveredbyP-invariants, then γisbounded.
Thereverse of (1)and (2)isnot true.
Theorem2
Let N bea PetriNet andi >0is a P-invariantofN. It holdsthat:
•||i||=||i||•
MSD (2020) Lecture4 5/ 41

LinearAlgebraicTechniques TransitionInvariants
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 6/ 41

LinearAlgebraicTechniques TransitionInvariants
TransitionInvariants
Decribe sequencesoftransitionswhich lead froma markingto the s ame marking.
Definition 2
Amarking M of a PetrinetN isreproducible if thereexists a non-e mptysequence of
transitionsw such thatM [w/an}bracketri}htM.
MSD (2020) Lecture4 7/ 41

LinearAlgebraicTechniques TransitionInvariants
TransitionInvariants- Definitions
Definition 3
Let N= (P,T,F,W)be a markedPetrinet. A T-invariant of N isanyn-dimensional
column vector j ∈Znforwhich C ·j=0, whereC isthe incidence matrixof N.
AnetNissaid to have T-invariantsif it hasat least non-nullT-invar iant.
MSD (2020) Lecture4 8/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariantsandReproducible Markings
Theorem3
APetrinetN haspositive T-invariantsiff N hasreproduciblemar kings.
MSD (2020) Lecture4 9/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariantsandReproducible Markings
Theorem3
APetrinetN haspositive T-invariantsiff N hasreproduciblemar kings.
(=⇒): Letj>0aT-invariantof N. LetMbea markinggivenby
M(p) =/summationdisplay
tk∈p•j(k)·W(p,tk),
foranyp∈P.
Consider thesequenceof transitions:
w=tj(1)
1…tj(n)
n
It holds:M[w/an}bracketri}htM′.
MarkingMis reproducible.
(⇐=)LetM[w/an}bracketri}htM. ThenM=M+C·− →w. HenceC·− →w=0and− →wis aT-invariant.
MSD (2020) Lecture4 9/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariantsCovering
Definition 4
Let N= (P,T,F,W)be a Petrinet. N is covered byT-invariants iff thereexists a
T-invariantj >0with||j||=T
MSD (2020) Lecture4 10/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariants,Livenessand Boundness
Theorem4
Anylive and boundedmarkedPetrinet iscovered byT-invarian ts.
MSD (2020) Lecture4 11/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariants,Livenessand Boundness
Theorem4
Anylive and boundedmarkedPetrinet iscovered byT-invarian ts.
In aliveandboundedPetri net,there exists a reachablemarking M∈[M0/an}bracketri}htandatransition sequence σsuch
that
σcontains allthe transitions in T
M[σ/an}bracketri}htM
j=− →σis aT-invariantwith ||j||=T.
MSD (2020) Lecture4 11/ 41

LinearAlgebraicTechniques TransitionInvariants
T-invariants,Livenessand Boundness
Theorem4
Anylive and boundedmarkedPetrinet iscovered byT-invarian ts.
t1p1t3
p2t2/parenleftigg
1 1 −1
0−1 1/parenrightigg
·
x
y
z
=0=⇒
/braceleftigg
x+y−z=0
−y+z=0
T-invariants: (0,α,α).
Thenet is notliveor itis not bounded.
MSD (2020) Lecture4 11/ 41

LinearAlgebraicTechniques TransitionInvariants
TransitionInvariants
Thereexist Petrinetscoveredby T-invariantswhich arenot liv e/bounded:
p1 t1 p3
p2 t2t3

−1 1 0
1−1 0
1 0 −1
·
x
y
z
=0
T-invariants: (α,α,α)T
Thenet iscovered byT-invariantsbut it isnot bounded.
MSD (2020) Lecture4 12/ 41

Structural AnalysisofPetri Nets Siphons
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 13/ 41

Structural AnalysisofPetri Nets Siphons
Siphons- definition
Definition 5
Let N= (P,T,F,W)be a Petrinet and R ⊆P a set of places. R iscalled a siphon if
•R⊆R•. Asiphon is properif R /ne}ationslash=∅.
MSD (2020) Lecture4 14/ 41

Structural AnalysisofPetri Nets Siphons
Siphons- definition
Definition 5
Let N= (P,T,F,W)be a Petrinet and R ⊆P a set of places. R iscalled a siphon if
•R⊆R•. Asiphon is properif R /ne}ationslash=∅.
{p1,p2}isa siphon.
MSD (2020) Lecture4 14/ 41

Structural AnalysisofPetri Nets Siphons
FundamentalPropertyof Siphons
Notations: let R⊆Pbe a set of placesand Ma marking. M(R) =/summationtext
p∈RM(p)
MSD (2020) Lecture4 15/ 41

Structural AnalysisofPetri Nets Siphons
FundamentalPropertyof Siphons
Notations: let R⊆Pbe a set of placesand Ma marking. M(R) =/summationtext
p∈RM(p)
Definition 6
LetN= (P,T,F,W)beaPetrinet,R ⊆P apropersiphonandM amarkingofN. R is
markedat M , if M (R)/ne}ationslash=0.
MSD (2020) Lecture4 15/ 41

Structural AnalysisofPetri Nets Siphons
FundamentalPropertyof Siphons
Notations: let R⊆Pbe a set of placesand Ma marking. M(R) =/summationtext
p∈RM(p)
Definition 6
LetN= (P,T,F,W)beaPetrinet,R ⊆P apropersiphonandM amarkingofN. R is
markedat M , if M (R)/ne}ationslash=0.
Proposition1 (Fundamentalpropertyof siphons)
Let N= (P,T,F,W)be a Petrinet and R ⊆P a propersiphon. LetM be a markingof
the netsuch that M (R) =0. Then,∀M′∈[M/an}bracketri}ht, M′(R) =0.
MSD (2020) Lecture4 15/ 41

Structural AnalysisofPetri Nets Siphons
Example
[M0/an}bracketri}ht={(0,0,1,0),(0,0,0,1)},{p1,p2}arenever marked.
MSD (2020) Lecture4 16/ 41

Structural AnalysisofPetri Nets Siphons
FundamentalPropertyof Siphons
Anecessarycondition for reachabilityisobtained
IfRisa siphon with M0(R) =0 andM(R)/ne}ationslash=0, thenM/ne}ationslash∈[M0/an}bracketri}ht.
R={p1,p2}siphon,M0(R) =0⇒markingM= (1,0,0,1)isnot reachable.
MSD (2020) Lecture4 17/ 41

Structural AnalysisofPetri Nets Siphons
Example
Proposition2
Letγ= (N,M0)bea marked Petrinet with W (f) =1,∀f∈F and M a marking. If M is
a deadmarking, then theset of placesR ={p∈P|M(p) =0}is aproper siphon.
MSD (2020) Lecture4 18/ 41

Structural AnalysisofPetri Nets Siphons
Example
Proposition2
Letγ= (N,M0)bea marked Petrinet with W (f) =1,∀f∈F and M a marking. If M is
a deadmarking, then theset of placesR ={p∈P|M(p) =0}is aproper siphon.
M= (0,0,1,0)isa dead marking,so {p1,p2,p4}isa siphon .
MSD (2020) Lecture4 18/ 41

Structural AnalysisofPetri Nets Siphons
Example
Proposition2
Letγ= (N,M0)bea marked Petrinet with W (f) =1,∀f∈F and M a marking. If M is
a deadmarking, then theset of placesR ={p∈P|M(p) =0}is aproper siphon.
Proposition3
Let N= (P,T,F,W)be a Petrinet i a P-invariantforN. Thesupport set, ||i||, isa
siphon.
MSD (2020) Lecture4 18/ 41

Structural AnalysisofPetri Nets Traps
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 19/ 41

Structural AnalysisofPetri Nets Traps
Traps-definition
Definition 7
Let N= (P,T,F,W)be a netand R ⊆P a set ofplaces. R is called a trapif R • ⊆ •R.
Atrap isproperif R /ne}ationslash=∅.
MSD (2020) Lecture4 20/ 41

Structural AnalysisofPetri Nets Traps
Traps-definition
Definition 7
Let N= (P,T,F,W)be a netand R ⊆P a set ofplaces. R is called a trapif R • ⊆ •R.
Atrap isproperif R /ne}ationslash=∅.
{p3,p4}isa trap.
MSD (2020) Lecture4 20/ 41

Structural AnalysisofPetri Nets Traps
Traps-definition
Definition 7
Let N= (P,T,F,W)be a netand R ⊆P a set ofplaces. R is called a trapif R • ⊆ •R.
Atrap isproperif R /ne}ationslash=∅.
Proposition4
Let N= (P,T,F,W)be a netand i a P-invariantof N. The supportset, ||i||, isa trap.
MSD (2020) Lecture4 20/ 41

Structural AnalysisofPetri Nets Traps
FundamentalPropertyof Traps
Proposition5
Let N= (P,T,F,W)be a Petrinet and R ⊆P a propertrap. Let M bea marking of
the netsuch that M (R)/ne}ationslash=0. Then,∀M′∈[M/an}bracketri}ht, M′(R)/ne}ationslash=0.
MSD (2020) Lecture4 21/ 41

Structural AnalysisofPetri Nets Traps
FundamentalPropertyof Traps
Proposition5
Let N= (P,T,F,W)be a Petrinet and R ⊆P a propertrap. Let M bea marking of
the netsuch that M (R)/ne}ationslash=0. Then,∀M′∈[M/an}bracketri}ht, M′(R)/ne}ationslash=0.
{p3,p4}isa trap.
Placesp3,p4remainmarked in anyreachablemarking.
MSD (2020) Lecture4 21/ 41

Structural AnalysisofPetri Nets Traps
FundamentalPropertyof Traps
Anecessarycondition for reachabilityisobtained
Given a marking MandRa trapwith M0(R)/ne}ationslash=0,ifM(R) =0, thenM/ne}ationslash∈[M0/an}bracketri}ht
R={p1,p2,p3}trap,M0(R)/ne}ationslash=0.
M= (0,0,0,1)/ne}ationslash∈[M0/an}bracketri}ht(M(R) =0)
MSD (2020) Lecture4 22/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 23/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Anecessarycondition forliveness
Proposition6
Letγ= (N,M0)bea live markedPetrinet . Anysiphon R of N ismarked at M 0.
MSD (2020) Lecture4 24/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Anecessarycondition forliveness
Proposition6
Letγ= (N,M0)bea live markedPetrinet . Anysiphon R of N ismarked at M 0.
{p1,p2}isnot markedat the initialmarking, hence thenet isnot live.
MSD (2020) Lecture4 24/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Anecessarycondition forliveness
Thereverse isnot true:
Allsiphonsaremarked in the initialmarking:
{p1,p2}
Thenet isnot live.
MSD (2020) Lecture4 25/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Deadlocks
Proposition7
Letγ= (N,M0)bea marked Petrinet with W (f) =1,∀f∈F. If anypropersiphon ofN
includesa trap markedat M 0, thenγisdeadlock-free.
MSD (2020) Lecture4 26/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Deadlocks
Proposition7
Letγ= (N,M0)bea marked Petrinet with W (f) =1,∀f∈F. If anypropersiphon ofN
includesa trap markedat M 0, thenγisdeadlock-free.
Siphons: {p1,p2},{p1,p2,p3},
Traps:{p1,p2},{p3},{p1,p2,p3}
Thenet is deadlock-free.
MSD (2020) Lecture4 26/ 41

Structural AnalysisofPetri Nets Siphons,TrapsandBehaviouralPropertiesofPetri Nets
Deadlocks
Thereverse isnot true:
p1 p2 p3 t1
t2t3 t4
Deadlock-free net
Propersiphons: {p1,p2}
Propertraps: {p3}
MSD (2020) Lecture4 27/ 41

Structural AnalysisofPetri Nets The cs-property
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 28/ 41

Structural AnalysisofPetri Nets The cs-property
Notations
Let(N,M0)bea marked Petrinet and pa place of N.
minp•=mint∈p•W(p,t)
maxp•=maxt∈p•W(p,t)
MSD (2020) Lecture4 29/ 41

Structural AnalysisofPetri Nets The cs-property
Min-controlled/max-controlledsiphons
Definition 8
Let(N,M0)bea marked Petrinet . A siphon S ismin-controlled(min-cs) if:
∀M∈[M0/an}bracketri}ht,∃p∈S:M(p)≥minp•.
(N,M0)satisfiesthe min-cspropertyif allitssiphons satisfythe min-cspr operty.
Definition 9
Asiphon S ismax-controlled (max-cs)if:
∀M∈[M0/an}bracketri}ht,∃p∈S:M(p)≥maxp•.
(N,M0)satisfiesthe max-cspropertyif allitssiphonssatisfy the max-cspr operty.
MSD (2020) Lecture4 30/ 41

Structural AnalysisofPetri Nets The cs-property
Thecs-property
Definition 10
APetrinet (N;M0)is said to besatisfying thecontrolled-siphon property(cs-prope rty)
if and onlyif each minimalsiphon of (N;M0)is min ormaxcontrolled.
a max-controlledsiphon isalso a min-controlled siphon
If∀t,t′∈p•:W(p,t) =W(p,t′), thena min-controlled siphonis also a
max-controlledsiphon.
MSD (2020) Lecture4 31/ 41

Structural AnalysisofPetri Nets The cs-property
Example
{p1,p2}min-cs, not max-cs
{p3}max-cs,min-cs
Thenet hasthe min-cspropertyandthe cs-property
MSD (2020) Lecture4 32/ 41

Structural AnalysisofPetri Nets The cs-property
Properties
Proposition8
If a markedPetrinet (N,M0)islive, thenit satisfiesthe min-csproperty.
Proposition9
If a markedPetrinet (N,M0)satisfies themax-csproperty, thenit is deadlock-free.
MSD (2020) Lecture4 33/ 41

Structural AnalysisofPetri Nets The cs-property
Example
{p1,p2}min-cs, not max-cs
{p3}max-cs,min-cs
min-cs, notlive
deadlock-free,not max-cs
MSD (2020) Lecture4 34/ 41

SpecialClassesofPetri Nets S-systems
Overview
1Linear AlgebraicTechniques
Place Invariants
Transition Invariants
2StructuralAnalysisof PetriNets
Siphons
Traps
Siphons, Trapsand BehaviouralPropertiesof PetriNets
The cs- property
3SpecialClassesof PetriNets
S-systems
MSD (2020) Lecture4 35/ 41

SpecialClassesofPetri Nets S-systems
Definition of S-systems
Definition 11
AS-system (statemachine) isa markedPetrinet (N,M0), where N = (S,T,F,W)
such that:
W(x,y) =1,∀(x,y)∈F
|•t|=|t•|=1∀t∈T.
Theweight functionis usuallyomitted: N= (S,T,F).
p1 p2 p3
t2t3
t4t1
MSD (2020) Lecture4 36/ 41

SpecialClassesofPetri Nets S-systems
Propertiesof S-systems
Proposition10 (fundamentalpropertyof S-systems)
Let(N,M0)bea S-system. If M ∈[M0/an}bracketri}ht, then M 0(S) =M(S).
p1 p2 p3
t2t3
t4t1
Anecessarycondition for reachabilityin S-systems: M= (0,1,0),M(S)/ne}ationslash=M0(S),
henceM/ne}ationslash∈[M0/an}bracketri}ht
MSD (2020) Lecture4 37/ 41

SpecialClassesofPetri Nets S-systems
LivenessandBoundnessin S-systems
Theorem5 (boundness)
AS-system (N,M0)isbounded
MSD (2020) Lecture4 38/ 41

SpecialClassesofPetri Nets S-systems
LivenessandBoundnessin S-systems
Theorem5 (boundness)
AS-system (N,M0)isbounded
Theorem6 (liveness)
AS-system (N,M0)islive iff it is stronglyconnectedand M 0(S)/ne}ationslash=0.
MSD (2020) Lecture4 38/ 41

SpecialClassesofPetri Nets S-systems
LivenessandBoundnessin S-systems
Theorem5 (boundness)
AS-system (N,M0)isbounded
Theorem6 (liveness)
AS-system (N,M0)islive iff it is stronglyconnectedand M 0(S)/ne}ationslash=0.
p1 p2 p3 t1
t2t3 t4
MSD (2020) Lecture4 38/ 41

SpecialClassesofPetri Nets S-systems
Reachabilityin S-systems
Lemma1
Let(N,M0)astronglyconnected system and M,M′markingssuch that
M(S) =M′(S). ThenM [∗/an}bracketri}htM′.
MSD (2020) Lecture4 39/ 41

SpecialClassesofPetri Nets S-systems
Reachabilityin S-systems
Lemma1
Let(N,M0)astronglyconnected system and M,M′markingssuch that
M(S) =M′(S). ThenM [∗/an}bracketri}htM′.
Consequence 1
Let(N,M0)astronglyconnected system and M a marking such thatM (S) =M0(S).
ThenM ∈[M0/an}bracketri}ht.
MSD (2020) Lecture4 39/ 41

SpecialClassesofPetri Nets S-systems
Reachabilityin live S-systems
Theorem7 (reachability)
Let(N,M0)bea stronglyconnected S-systemand M one of itsmarkings. M is
reachable iff M (S) =M0(S)
MSD (2020) Lecture4 40/ 41

SpecialClassesofPetri Nets S-systems
Reachabilityin live S-systems
Theorem7 (reachability)
Let(N,M0)bea stronglyconnected S-systemand M one of itsmarkings. M is
reachable iff M (S) =M0(S)
(0,0,0,1,1)reachable fromthe initialmarking.
MSD (2020) Lecture4 40/ 41

SpecialClassesofPetri Nets S-systems
Propertiesof S-systems
Lemma1
Let(N,M0)bea connected S-system. Avector i :S→Zisa P-invariantof N iff
i= (x,x,…,x).
MSD (2020) Lecture4 41/ 41

SpecialClassesofPetri Nets S-systems
Propertiesof S-systems
Lemma1
Let(N,M0)bea connected S-system. Avector i :S→Zisa P-invariantof N iff
i= (x,x,…,x).
Theorem8
Let(N,M0)bea stronglyconnected S-systemand M a marking. M ∈[M0/an}bracketri}ht ⇔forevery
P-invarianti: i ·M=i·M0
MSD (2020) Lecture4 41/ 41