PTnet Definitions – Behavioural Properties
20/3/2014
CE-653 - PTnet Theory and some
Algorithms
9
}Definition [Bounded Net]:
}A marked net (N, M0) is bounded iff:
}for all p in S, there
exists k in N, s.t. for all markings M
reachable from M0: M(p) ≤ k
}Definition [Structurally Bounded Net]:
}A net N is structurally bounded iff it is bounded for
any initial marking M0.
}Definition [Liveness]:
}A transition t in T is live in (N, M0) iff:
}For all M in R(N, M0) there exists M’ in R(N, M): M’ enables
t.
}The marked net (N, M0) is live iff all t in T are
live.
}N is structurally live iff there exists initial
marking M0 such that (N, M0) is live