PetiNet 是 Peti 网系统

网

满足以下条件的三元组N=(S, T; F)被称为网:

(1) S \cup T \neq ∅;
(2) S \cap T = ∅;
(3) F ⊆ S × T ∪ T × S;
(4) dom(F ) ∪ cod(F ) = S ∪ T ;

其中，dom(F) = \{x|∃x : (x, y) \in F \}, cod(F) = \{y|∃x : (x, y) \in F \}。

这两个互不相交的集合S和T构成了网N的基础构成部分。其中S中的每一个成员被称作库所（place），而T中的每个成员则被称作变迁（transiton）。另外一种表示方法为将F定义为该网N的流动关联式

标识网

定义一个网N=(S,T;F)。映射M:s\to\{0,1,2...\} 被称作网N的一个标记符。（也即四元组(S,T;F,M)）被称为一个标记网络。

Petri网

注意

对于变换t\in T而言，在集合\forall s \in S: s\in \bullet t \to M(s)\ge 1,的情况下，则称该变换t在标志M上有授权权，并以符号表示为：M[t]>

当状态机处于标记t’时，在其当前的状态为t’的情况下，则变迁$t’能够触发（即满足条件）。通过执行该变迁操作后会生成新的