零安全网合成：从线性步自动机到高效工作流建模

### 零安全网合成：从线性步自动机到高效工作流建模 在当今复杂的工作流系统中，如何确保系统的安全性和高效性是一个关键问题。零安全网（Zero-Safe nets，ZS-nets）作为一种强大的建模工具，为解决这一问题提供了有效的途径。本文将深入探讨零安全网的合成算法，以及它与线性步自动机之间的关系。 #### 零安全网合成算法概述 我们提出了一种算法，用于从有限的线性步自动机生成零安全网。在这个过程中，线性步自动机中的每个从状态 $q$ 到状态 $q'$ 的转换，都是正则语言 $L(q, q')$ 中的一个微步序列。合成的零安全网具有良好的行为特性，即从稳定标记出发的任何并发启用的转换序列都可以扩展为一个稳定步骤。这意味着在由零安全网合成实现的工作流中，不需要进行补偿操作。 然而，由于零安全网的注入式标记，某些线性步自动机可能无法由任何行为良好的零安全网实现。因此，我们还提出了一个决策和合成算法，其输出要么是一个实现输入线性步自动机的行为良好的零安全网，要么是不存在这样的网的答案。该算法的时间复杂度与步自动机的大小成多项式关系。 #### 零安全网的基本概念 在深入探讨算法之前，我们需要了解零安全网的基本概念。 - **PT 网**：PT 网是一个四元组 $N = (P, T, F, M_0)$，其中 $P$ 和 $T$ 分别是位置和转换的不相交集合，$F$ 是一个从 $(P × T) ∪ (T × P)$ 到自然数集 $\mathbb{N}$ 的映射，$M_0$ 是初始标记。标记是一个从 $P$ 到 $\mathbb{N}$ 的映射。如果对于每个位置 $p$，都有 $M(p) \geq F(p, t)$，则转换 $t$ 在标记 $M$ 下有许可，此时可以触发该转换。触发转换 $t$ 会导致标记 $M$ 变为 $M'$，满足 $M(p) - F(p, t) = M'(p) - F(t, p)$ 对于所有 $p$。 - **零安全网**：零安全网（ZS-net）是一种特殊的 PT 网，其中位置集 $P$ 可以分为两个不相交的子集 $S$ 和 $Z$，且对于所有 $z \in Z$，有 $M_0(z) = 0$。$S$ 中的位置称为稳定位置，$Z$ 中的位置称为零位置。如果对于每个零位置 $z \in Z$，都有 $M(z) = 0$，则标记 $M$ 是稳定的。 零安全网中的稳定步骤和稳定事务是两个重要的概念： - **稳定步骤**：一个非空的触发序列 $\rho = M_0[t_1\rangle... M_{n - 1}[t_n\rangle M_n$ 是零安全网的稳定步骤，当且仅当对于所有 $s \in S$，有 $\sum_{i = 1}^{n} F(s, t_i) \leq M_0(s)$（并发启用），并且 $M_0$ 和 $M_n$ 是稳定标记（稳定公平性）。 - **稳定事务**：一个稳定步骤 $\rho$ 是零安全网的稳定事务，当且仅当标记 $M_1,..., M_{n - 1}$ 不是稳定的（原子性），并且对于所有 $s \in S$，有 $\sum_{i = 1}^{n} F(s, t_i) = M_0(s)$（完美启用）。 零位置可以用于在单个事务中协调和同步任意数量的转换。在稳定事务中，输入到稳定位置的令牌（也称为稳定令牌）会被冻结，直到事务完成。这与线性步自动机中在步骤完成时更新当前状态的直觉是一致的。 #### 线性步自动机 线性步自动机是一个三元组 $A = (Q, L, q_0)$，其中 $Q$ 是状态集，$q_0$ 是初始状态，$L$ 是一个从 $Q × Q$ 到 $T^*$ 的幂集的映射，定义了从状态 $q$ 到状态 $q'$ 的非空微步序列的集合 $L(q, q')$。 线性步自动机具有以下性质： - **可达性**：如果对于任意状态 $q \in Q$，都存在一个序列 $q_0q_1... q_n$，使得对于所有 $i$，有 $L(q_i, q_{i + 1}) \neq \varnothing$，则线性步自动机是可达的。 - **正则性**：如果 $Q$ 是有限的，并且所有语言 $L(q, q')$ 都是 $T^*$ 的正则子集，则线性步自动机是正则的。 - **平凡性**：如果线性步自动机只有一个状态 $q_0$，并且 $L(q_0, q_0) = \varnothing$，则它是平凡的。 一般来说，线性步自动机可能是非确定性的，并且 $L(q, q')$ 和 $L(q, q'')$ 可能有交集，$L(q, q') L(q', q'')$ 可能与 $L(q, q'')$ 及其补集都有交集。 #### 零安全网与线性步自动机的关系 一个零安全网实现一个线性步自动机，当且仅当该自动机可以作为零安全网的抽象（在同构意义下）被重构。我们考虑的抽象是可达稳定状态图（Reachable Stable State Graph，RSSG）。 设 $N = (S ∪ Z, T, F, M_0)$ 是一个零安全网，其可达稳定标记集 $RSM(N)$ 是包含 $M_0$ 的最小稳定标记集，使得对于所有 $w \in T^*$，如果 $M \in RSM(N)$ 且 $M\{[w\rangle M'$，则 $M' \in RSM(N)$。可达稳定状态图 $RSSG(N)$ 是一个线性步自动机 $(RSM(N), L, M_0)$，其中 $L(M, M') = \{w | M\{[w\rangle M'\}$。 我们的目标是给定一个正则且可达的线性步自动机