Petri网

    Petri网是提出比较早且研究最好的可用于并发建模的流程建模语言。尽管图形表示法直观且简单，但是Petri网是可执行的，可以使用许多分析技术对其进行分析。Petri网是由库所（place）和变迁（transition）组成的二分图（bipartite）。网络结构是静态的，但是在触发规则（firing rule）的控制下，托肯（token）可以流经网络。 Petri网的状态由托肯在各库所的分布确定，并称为其标记（marking）。下图所示的初始标记中，只有一个托肯，start是唯一标记的库所。

图2 与图1对应的Petri网

    下面给出Petri网的形式化定义：
定义2（Petri网） 一个Petri网是一个三元组N = (P，T，F)，其中P是库所的有限集合，T是变迁的有限集合，并且P ∩T=∅，F⊆(P×T)∪(T×P)是有向弧的集合，称为流关系（flow relation）。一个标记Petri网以(N，M)对表示，其中N = (P，T，F)是一个Petri网，M∈