工作流网的健全性

工作流的每个中间局面都应保留完成的可能；一旦宣布完成，就不应还有遗留任务或多余完成 token；设计在图上的每项任务至少应有机会被使用。这三条分别约束恢复能力、完成标记和不可执行分支。

图上存在从起点到终点的路径远远不够。Petri 网同步需要同时拥有所有输入 token，单纯连通性看不见这项资源条件。

XOR 分流接 AND 汇合会卡住 ​

从 $i$ 有两条互斥变迁 $a:i\to p$、$b:i\to q$，终止变迁 $j:p+q\to o$。每个结点在图论上都位于 $i$ 到 $o$ 的路径上，所以它确为工作流网。

但从一个初始 token 只能选择 $a$ 或 $b$。选择 $a$ 后只有 $p$，选择 $b$ 后只有 $q$，$j$ 永远缺另一个输入。可完成性失败，$j$ 也是死变迁。修复时必须协调分流与汇合语义，例如并行分流 $i\to p+q$，或让两条分支分别单独汇入 $o$。

AND 分流后各自宣布完成也不对 ​

若先 $i\to p+q$，再分别用 $p\to o$、$q\to o$，第一次结束一条支线就到达 $[o]+[q]$ 或 $[p]+[o]$，违反干净完成；两条都结束则得到 $2[o]$，仍不是单实例终态。同步汇合应消耗两边 token 后只产生一个完成 token。

一个健全网仍可能一直绕圈 ​

考虑 $i\to p$、循环 $r:p\to p$、退出 $e:p\to o$。任何可达中间态都能选 $e$ 完成，完成时没有残留，三个变迁均有可执行机会，所以网健全。

但执行可以永远选择 $r$ 而不选 $e$。经典健全性没有强迫调度者退出；若需要所有执行终止，必须另加终止或公平性规格。把“总能完成”翻译成“必定完成”会错误拒绝或错误接受带重试的流程。

把新变迁 $t^{\ast }:o\to i$ 加到网中，得到短接网。对这里的普通工作流网，经典健全性等价于从 $[i]$ 出发的短接网既有界又活。[1, Lemma 5.1] 完成后可以重新开始，使“每个状态还可走到完成”和“每项任务以后仍可能发生”连起来；有界性排除反复循环积累未清理 token。

这不是任意扩展网的通用定理。重置弧、抑制弧、数据条件及多实例共享资源会改变结论。$k$-健全性从 $k[i]$ 出发要求干净到达 $k[o]$；单实例健全性不能自动推出所有 $k$ 的健全性。

安全与活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。提供另一种阅读方式：干净完成是排除坏状态，可完成性则要求每个可达状态保留一条好未来。后者是分支式存在未来，不是每条运行的必然活性。