工作流网的数据依赖与可达性分析

### 工作流网的数据依赖与可达性分析 在工作流管理中，对工作流网的研究至关重要。本文将围绕工作流网与数据的结合展开，详细探讨工作流网与数据（WFD - net）的相关概念、行为、可达性以及健全性等内容。 #### 工作流网与数据（WFD - net）的定义 在工作流网中引入数据元素和谓词是为了更精确地描述工作流的行为。我们假设存在一个有限的数据元素集合 \(D = \{d_1, \ldots, d_m\}\) 和一组谓词 \(\Pi = \{\pi_1, \ldots, \pi_n\}\)。同时，有一个谓词标记函数 \(\ell: \Pi \to 2^D\)，它为每个谓词分配其所依赖的数据元素集合。当 \(\ell(\pi) = \{d_1, \ldots, d_n\}\) 时，我们有时会写成 \(\pi(d_1, \ldots, d_n)\) 来强调这种依赖关系。 一个工作流网与数据（WFD - net） \(N = \langle P, T, F, rd, wt, del, grd\rangle\) 由以下部分组成： - 一个工作流网 \(\langle P, T, F\rangle\) - 读取数据标记函数 \(rd : T \to 2^D\) - 写入数据标记函数 \(wt : T \to 2^D\) - 删除数据标记函数 \(del : T \to 2^D\) - 保护函数 \(grd : T \to G_{\Pi}\)，为每个转换分配一个保护条件 例如，在一个托运人的工作流中，数据元素 \(D = \{cl, gds, ads, price, bon\}\)。对于转换“calculate bonus”，其标记函数为 \(rd(\text{calculate bonus}) = \{price\}\)，\(wt(\text{calculate bonus}) = \{bon\}\)，\(del(\text{calculate bonus}) = \varnothing\)，\(grd(\text{Ship normal}) = \neg\text{isHigh}(price)\)。 #### WFD - net 的语义 WFD - net 的模型是一个概念模型，用于描述多个可执行的工作流。我们引入基于超转换系统的特殊语义，以便在一个图中捕获 WFD - net 的所有可能细化。 ##### 行为分析 在 WFD - net 中，数据值未被明确指定，但我们可以区分已创建和未创建的数据值。通过三个抽象函数，我们为数据元素、谓词和保护条件分配抽象值。 - 函数 \(\sigma_D : D \to \{\top, \bot\}\) 为每个数据元素 \(d \in D\) 分配 \(\top\)（已定义值）或 \(\bot\)（未定义值） - 函数 \(\sigma_{\Pi} : \Pi \to \{T, F, \bot\}\) 为每个谓词分配真、假或未定义的值 一个状态 \(\sigma = (\sigma_D, \sigma_{\Pi})\)，所有状态的集合记为 \(\Sigma\)。我们使用简化符号 \(\sigma(d) = \sigma_D(d)\) 和 \(\sigma(\pi) = \sigma_{\Pi}(\pi)\)。 一个配置 \(c = \langle m, \sigma\rangle\) 由 WFD - net 的标记 \(m\) 和状态 \(\sigma\) 组成。初始配置中，只有起始位置被标记，所有数据元素和谓词都未定义。最终配置包含最终标记 \([end]\)。 转换 \(t\) 在配置 \(c = \langle m, \sigma\rangle\) 中被启用需要满足两个条件： 1. 转换 \(t\) 在标记 \(m\) 下被启用 2. 转换 \(t\) 读取的数据元素和其保护条件中的谓词所依赖的数据元素都已定义，且保护条件评估为真 启用的转换 \(t\) 触发后，会改变标记和数据元素的值。由于我们不知道具体操作和谓词的值，触发 \(t\) 会产生一组后续配置 \(\langle m', \sigma'\rangle\)。 下面是触发规则的详细定义： 设 \(N = \langle P, T, F, rd, wt, del, grd\rangle\) 是一个 WFD - net。转换 \(t \in T\) 在配置 \(c = \langle m, \sigma\rangle\) 中被启用，当且仅当 \(m \xrightarrow{t}\)，所有 \(d \in rd(t)\) 已定义，所有分配给 \(t\) 的转换保护条件 \(grd(t)\) 中的谓词的数据元素都已定义，且 \(\sigma(grd(t)) = T\)。触发 \(t\) 产生一组配置 \(C \subseteq \Sigma\)，其中 \(C = \{\langle m', \sigma'\rangle | m \xrightarrow{t} m' \land (\forall d \in del(t) : \sigma'(d) = \bot \land \forall \pi \in \Pi : d \in \ell(\pi) \Rightarrow \sigma'(\pi) = \bot) \land (\forall d