Petri网
Petri网使用简单的图形较好地表示并发、同步、因果等关系，以网图的形式简洁、直观地模拟离散事件系统。
基本概念
Petri网是一种网状信息流模型，包括条件和事件两类节点，在条件和事件为节点的有向二分图基础上添加表示状态信息的token分布，并按引发规则使得事件驱动状态演变，从而反映系统动态运行过程。
| 元素 | 表示 |
|---|---|
| 小矩形 | 事件（变迁）结点 |
| 小圆形 | 条件（位置）结点 |
| 有向弧 | 变迁结点之间、位置结点之间不能有有向弧，变迁结点与位置节点之间连接有向弧 |
| 若干黑点 | 网的某些位置结点中标上的token |
由此构成的有向二分图称作网，从而构成Petri网。
| 组成 | 概念 |
|---|---|
| 资源 | 与系统状态变化有关的因素，如原料、产品、工具、设备等 |
| 状态元素 | 资源归类后的抽象 |
| 库所 | 一个场所，存放状态元素 |
| 变迁 | 资源状态变化 |
| 事件 | 引起条件的变迁称为事件 |
| 容量 | 库所的最大资源数量 |
一个Petri网是一个三元组 $N = (P, T, F)$，其中：
- $P = \{p_1, p_2, \cdots, p_m\}$ 为库所的集合
- $T = \{t_1, t_2, \cdots, t_n\}$ 为变迁的集合
- $F = (P \times T) \cup (T \times P)$ 为输入函数和输出函数集，称为流关系。
约束：
- $P \cap T = \oslash$，规定了库所和变迁是两类不同的元素
- $P \cup T \ne \oslash$，表示网中至少有一个元素
- $F = (P \times T) \cup (T \times P)$ 建立了从库所到变迁、从变迁到库所的单方向联系，并且规定同类元素之间不能直接联系
在有向图 $N = (P, T, F)$ 中，
- 设 $K: P \rightarrow \{1, 2, 3, \cdots \}$ 表示 $N$ 上 $P$ 的容量，用库所中的黑点表示（无黑点表示无穷大）；
- 设 $W: F \rightarrow \{1, 2, 3, \cdots \}$ 表示 $N$ 上 $F$ 的权重，用有向弧上的数字表示（无数字表示权重是1）
| 分类 | |
|---|---|
| 基本Petri网 | 每个库所容量为1，这时库所可称为条件，变迁可称为事件。故又称为条件/事件系统（C/E） |
| 低级Petri网 | 库所容量和权重为>=1的任意整数，称为库所/变迁网（P/T） |
| 定时Petri网 | 将各事件的持续时长标在库所旁边，库所中新产生的标记经过一须时间后才加入到网中，或是标在变迁上，经过时间延迟后发生 |
| 高级Petri网 | 谓词/事件网、染色网、随机网等 |
行为特性
Petri网具有一些专门的分析手段，对系统活性和死锁进行分析。分析系统中的顺序、并发及冲突等复杂事件的关系。
可达性
可达性是研究任何系统动态特性的基础，决定系统能否到达一个指定的状态。
系统按照一定的流程运行，系统是否能够实现一定的状态；或者不期望的状态不出现。或者要求到达一定的状态，如何确定系统的运行轨迹（流程）
活性
在系统中用于检测是否存在死锁。一个系统存在的一个潜在问题是死锁，为了避免死锁， 系统的Petri网模型必须具有活性。
解决死锁的方法：
- 互斥：同时争夺唯一资源
- 占用且等待
- 无抢占
- 循环等待
有界性
有界性是一个非常重要的特性，它保证系统在运行过程中不会需要无限的资源
有界性反映一个库所在系统运行过程中能够获得的最大的令牌数，即所能获得的最大资源数，它与系统的初始令牌有关.
在实际系统设计中，必须使网络中的每个库所在任何状态下的令牌数小于库所的容量，这样才能保证系统的正常运行。
安全性
安全性决定系统中正在执行的操作不会发出请求。若Petri网为1有界，则称此Petri网是安全的。这种网的每一个库所要么有一个令牌，要么没有令牌。
安全性是有界性的一种特殊情况 。
可逆性和回家状态（主宿状态）
在制造业系统和过程控制系统中存在着一个重要的问题：错误复原，即系统能否重新回到原来状态（保证系统的循环特性）。
可逆：系统可自生初始化
主宿（回家）：系统经过有限步骤将回到期望状态
守恒性
在一个Petri网系统中，令牌被用来描述系统资源。对这类Petri网，守恒性是一个重要性质，要使代表资源的令牌在Petri网运行中既不会增加也不会减少，最简单的方法就是网中总令牌数保持恒定。
Petri网的应用
描述系统
Petri网描述系统的最基本概念是库所和变迁
库所表示系统的状态。变迁表示资源的消耗、使用及使系统状态产生的变化。
变迁的发生受到系统状态的控制，即变迁发生的前置条件必须满足；变迁发生后，某些前置条件不再满足，而某些后置条件则得到满足。
用圆圈表示为库所，粗实线表示变迁，联结库所与变迁之间的有向弧表示输入输出函数，用令牌（token）表示库所中拥有的资源数量（黑点或数字表示）
分析系统故障
Petri网是一种图形演绎方法，应用Petri网分析系统故障就是将系统所不希望发生的事件作为顶库所，逐步找出导致这一事件的所有可能因素作为中间库所和底库所。
故障树可以看作是系统中故障传播的逻辑关系，一般的单调关联故障树只含有与门和或门。故障树可以很方便地用Petri网表示，如与门采用多输入变迁代替，或门采用两个变迁代替。
在故障树分析中，当一些底事件同时发生时，顶事件必然发生，能使顶事件发生的这些底事件的集合就称为割集。如果割集中的任一底事件不发生时，顶事件也不发生，则这样的割集称为最小割集。
关联矩阵是Petri网的主要分析方法之一:
- 若从库所 $P$ 到变迁 $t$ 的输入函数取值为非负整数 $w$，记为 $I(P,t)=w$，用从 $P$ 到 $t$ 的一有向弧并旁注 $w$ 表示
- 若从变迁 $t$ 到库所 $P$ 的输出函数取值为非负整数 $w$，记为 $O(P,t)=w$，用从 $t$ 到 $P$ 的一有向弧并旁注 $w$ 表示
- $O$ 与 $I$ 之差 $A^T=O-I$ 称为关联矩阵。这里我们探讨规范网，所以 $w=1$。
特别地，若 $w=1$，则不必标注；若 $I(P,t)=0$ 或 $O(P,t)=0$，则不必画弧。$I$ 与 $O$ 均可表示为 $n \times m$ 非负整数矩阵。
例如，对于如下的Petri网：
有
$$ \bm{I} = \left[ \begin{matrix} 1 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 1 & 0 \\ 0 & 0 & 0 \end{matrix} \right]，\bm{O} = \left[ \begin{matrix} 0 & 0 & 0 \\ 0 & 0 & 0 \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \end{matrix} \right]$$则
$$\bm{A}^T = \bm{O}-\bm{I} = \left[ \begin{matrix} -1 & 0 & 0 \\ -1 & 0 & 0 \\ 0 & 0 & -1 \\ 1 & -1 & 0 \\ 0 & 1 & 1 \end{matrix} \right]$$割集求解步骤
- 找出关联矩阵中只有 $1$ 和 $0$，没有 $-1$ 的行，则该行对应的为顶库所（只有输入库所，没有输出库所），由此库所开始寻找（在此关联矩阵中为最后一行）。
- 由顶库所对应行的 $1$ 出发按列寻找到 $-1$，此 $-1$ 所对应行代表的库所为顶库所的一个输入库所，如果该列有多个 $-1$，则说明对应同一变迁有多个输入库所，并且输入的库所为“与”关系。
- 由步骤2中找到的 $-1$ 按行寻找 $1$，如有 $1$ 则说明该库所为中间库所，继续按步骤2所述循环查找，直到所在行没有 $1$ 为止。没有 $1$，则说明该库所是一个底库所即基本事件。如果该行有多个 $1$，则说明由这些1对应的库所对应多个变迁，应为“或”关系。
- 按步骤2、步骤3继续查找，直到查找到最底层的库所
- 按照上面的“与”“或”关系将底库所展开，则得到所有割集。
- 按照布尔吸收律、等幂率或素数法可求得最小割集
动态系统
转换系统是描述硬件/软件系统中计算/通信的常用语义模型。
系统结构
一个动态系统的形式化定义为一个元组 $\left<S, \text{Act}, \rightarrow, I, \text{AP}, L\right>$，其中：
- $S$ 是一系列状态。
- $\text{Act}$ 是一系列行为。
- $\rightarrow \subseteq S \times \text{Act} \times S$ 是一个转换关系。
- $I \subseteq S$ 是一系列初始状态。
- $\text{AP}$ 是一系列原子命题。
- $L: S \rightarrow 2^{AP}$ 是一个函数。
前驱和后继
$$\text{Pre}(s, \alpha) = \{s' = S \mid s' \xrightarrow{\alpha} s\}, \qquad \text{Pre}(s) = \bigcup_{\alpha \in \text{Act}} \text{Pre}(s, \alpha)$$$$\text{Post}(s, \alpha) = \{s' = S \mid s \xrightarrow{\alpha} s'\}, \qquad \text{Post}(s) = \bigcup_{\alpha \in \text{Act}} \text{Post}(s, \alpha)$$$$\text{Pre}(C, \alpha) = \bigcup_{s \in C} \text{Pre}(s, \alpha), \qquad \text{Pre}(C) = \bigcup_{s \in C} \text{Pre}(s) \text{ for } C \subseteq S$$$$\text{Post}(C, \alpha) = \bigcup_{s \in C} \text{Post}(s, \alpha), \qquad \text{Post}(C) = \bigcup_{s \in C} \text{Post}(s) \text{ for } C \subseteq S$$终止条件
状态 $s$ 终止当且仅当 $\text{Post}(s)=\oslash$
在如图所示的自动售货机系统中，有
- $S = \{\text{pay}, \text{select}, \text{soda}, \text{beer}\}$
- $\text{Act} = \{\text{insert\_coin}, \text{get\_soda}, \text{get\_beer}, \tau\}$
- $I = \{\text{pay}\}$
- $\text{AP} = \{\text{paid}, \text{drink}\}$
- $L(\text{pay}) = \oslash$，$L(\text{select}) = \{\text{paid}\}$，$L(\text{soda}) = L(\text{beer}) = \{\text{paid}, \text{drink}\}$
它的前驱和后继分别有：
- $\text{Post}(\text{pay}, \text{insert\_coin}) = \{\text{select}\}$
- $\text{Pre}(\text{pay}, \text{get\_soda}) = \{\text{soda}\}$
- $\text{Pre}(\text{pay}) = \{\text{soda}, \text{beer}\}$
确定性变迁
记 $\text{TS} = (S, \text{Act}, \rightarrow, I, \text{AP}, L)$：
若 $\forall s,\alpha$，都有 $|I| < 1$ 且 $|\text{Post}(s, \alpha)| \leqslant 1$，则称 $TS$ 为动作确定性的系统
即对于同一行动，不超过2个后继。
若 $\forall s, A \in 2^{\text{AP}}$，都有 $|I| \leqslant 1$ 且 $|\text{Post}(s) \cap \{s' \in S \mid L(s') = A\}| \leqslant 1$
即同一标签的后继不超过2个。
动作执行
执行（运行）是状态转换的线性序列，用于描述系统的动态行为。
动态系统 $\text{TS}$ 的有限执行片段 $\rho$ 是以状态结尾的、状态和动作交替的序列：
$$\rho = s_o \alpha_1 s_1 \alpha_2 \cdots \alpha_n s_n$$其中 $\forall\ 0 \leqslant i < n$，有 $s_i \xrightarrow{\alpha_{i+1}} s_{i+1}$
相应的，动态系统 $\text{TS}$ 的无限执行片段 $\rho$ 可表示为
$$\rho = s_o \alpha_1 s_1 \alpha_2 s_2 \alpha_3 \cdots$$其中 $\forall\ i \geqslant 0$，有 $s_i \xrightarrow{\alpha_{i+1}} s_{i+1}$
如果 $s_0 \in I$，则称该执行为初始执行。
最大执行片段可以是有限的，以终端状态结束；也可以是无限的
可达状态
如果存在初始的有限执行片段，则状态 $s \in S$ 在 $\text{TS}$ 中称为可达
$$s_0 \xrightarrow{\alpha_1} s_1 \xrightarrow{\alpha_2} s_2 \cdots \xrightarrow{\alpha_n} s_n = s$$记 $\text{Reach}(\text{TS})$ 表示 $\text{TS}$ 中所有可到达状态的集合。
几种系统
程序图
定义在类型变量集Var上的程序图 $\text{PG}$ 可表示为一个元组
其中：
- $\text{Loc}$ 是一组位置，初始位置记为 $\text{Loc}_0 \subseteq \text{Loc}$。
- $\text{Act}$ 是一系列行为。
- $\text{Effect}: \text{Act} \times \text{Eval(Var)} \rightarrow \text{Eval(Var)}$ 是结果函数。
- $\hookrightarrow \subseteq \text{Loc} \times \text{Cond(Var)} \times \text{Act} \times \text{Loc}$ 是转换关系。
- $g_0 \in \text{Cond(Var)}$ 是初始条件。
程序图 $\text{PG} = (\text{Loc}, \text{Act}, \text{Effect}, \hookrightarrow, \text{Loc}_0, g_0)$ 的转换可以表示为
$$(S, \text{Act}, \rightarrow, I, \text{AP}, L)$$其中：
- $S = \text{Loc} \times \text{Eval(Var)}$
- $\rightarrow \subseteq S \times \text{Act} \times S$ 定义为 $$\frac{l \xhookrightarrow{g: \alpha} l' \land \eta \vDash g}{\left< l, \eta \right> \xrightarrow{\alpha} \left< l', \text{Effect}(\alpha, \eta) \right>}$$
- $I = \{\left< l, \eta \right> \mid l \in \text{Loc}_0, \eta \vDash g_0\}$
- $L(\left< l, \eta \right>) = \{l\} \cup \{g \in \text{Cond(Var)} \mid \eta \vDash g\}$
对于一个给定的程序图，它的可能状态数有
$$|\text{Loc} | \cdot \prod_{x \in \text{Var}} |\text{dom}(x)|$$并发系统
交错执行是解决并发系统冲突的有效方法。
设 $\text{TS}_i = (S_i, \text{Act}_i, \rightarrow_i, I_i, \text{AP}_i, L_i)$，其中 $i=1,2$ 为两个转换系统，则它们的并发表示为
$$\text{TS}_1 ||| \text{TS}_2 = (S_1 \times S_2, \text{Act}_1 \cup \text{Act}_2, \rightarrow, I_1 \times I_2, \text{AP}_1 \cup \text{AP}_2, L)$$其中 $L(\left< s_1, s_2\right>) = L_1(s_1) \cup L_2(s_2)$，$\rightarrow$ 定义为
$$\frac{s_1 \xrightarrow{\alpha}_1 s'_1}{\left< s_1, s_2\right> \xrightarrow{\alpha} \left< s'_1, s_2 \right>} \qquad \frac{s_2 \xrightarrow{\alpha}_2 s'_2}{\left< s_1, s_2\right> \xrightarrow{\alpha} \left< s_1, s'_2 \right>}$$假设 $\text{TS}_1$ 和 $\text{TS}_2$ 是独立的，即没有共享的动作或变量。
同时执行的独立动作 $\alpha$ 和 $\beta$ 的效果等于 $\alpha$ 和 $\beta$ 以任意顺序连续执行时的效果
访问共享变量的操作是关键的，否则它们是非关键的。非关键操作可以与任何其他操作并行执行。并发关键操作的执行顺序会影响全局状态
记 $\text{TS} = \text{TS}_1 \parallel \text{TS}_2 \cdots \parallel \text{TS}_n$。它的可能状态数有
$$|S_1| \cdot |S_2| \cdots \cdot |S_n|$$联络
设 $\text{TS}_i = (S_i, \text{Act}_i, \rightarrow_i, I_i, \text{AP}_i, L_i)$，其中 $i=1,2$，$H \subseteq \text{Act}_1 \cap \text{Act}_2$，则有
$$\text{TS}_1 \parallel_H \text{TS}_2 = (S_1 \times S_2, \text{Act}_1 \cup \text{Act}_2, \rightarrow, I_1 \times I_2, \text{AP}_1 \cup \text{AP}_2, L)$$其中 $L(\left< s_1, s_2\right>) = L_1(s_1) \cup L_2(s_2)$，
$\rightarrow$ 对 $\alpha \notin H$ 定义为
$$\frac{s_1 \xrightarrow{\alpha}_1 s'_1}{\left< s_1, s_2\right> \xrightarrow{\alpha} \left< s'_1, s_2 \right>} \qquad \frac{s_2 \xrightarrow{\alpha}_2 s'_2}{\left< s_1, s_2\right> \xrightarrow{\alpha} \left< s_1, s'_2 \right>}$$对 $\alpha \in H$ 定义为
$$\frac{s_1 \xrightarrow{\alpha}_1 s'_1 \land s_2 \xrightarrow{\alpha}_2 s'_2}{\left< s_1, s_2 \right> \xrightarrow{\alpha} \left< s'_1, s'_2\right>}$$同步
设 $\text{TS}_i = (S_i, \text{Act}_i, \rightarrow_i, I_i, \text{AP}_i, L_i)$，其中 $i=1,2$，定义
$$\text{TS}_1 \otimes \text{TS}_2 = (S_1 \times S_2, \text{Act}_1 \times \text{Act}_2, \rightarrow, I_1 \times I_2, \text{AP}_1 \cup \text{AP}_2, L)$$其中 $L(\left< s_1, s_2\right>) = L_1(s_1) \cup L_2(s_2)$，$\rightarrow$ 定义为
$$\frac{s_1 \xrightarrow{\alpha}_1 s'_1 \land s_2 \xrightarrow{\beta}_2 s'_2}{\left< s_1, s_2\right> \xrightarrow{(\alpha, \beta)} \left< s'_1, s_2 \right>}$$