单计数器网络上的模拟与双模拟关系研究

### 单计数器网络上的模拟与双模拟关系研究 在自动形式验证领域，无限状态过程的有限描述至关重要。因为验证工具通常仅适用于有限状态系统，而实际分析的系统虽语义上是有限状态，但语法上常表达为无限状态系统。本文将围绕单计数器网络展开，探讨模拟关系的构建以及相关性质的判定。 #### 规则性与强规则性 规则性和强规则性意味着一个过程在某种等价意义下可以有限表示。规则性表示存在一个等价的有限状态过程；强规则性则要求其状态空间在等价关系下的商是有限的。所有“合理”的过程等价关系在各自的商下是保持不变的，强规则性实际上保证了存在一个状态空间相同（在等价意义下）的有限状态过程，它能比仅等价的过程保留更多的逻辑属性。 #### 研究问题概述 我们将解决以下几个重要问题： 1. 构建给定单计数器网络的最大模拟关系的描述。 2. 研究模拟和双模拟关系之间的联系。 3. 判定单计数器网络的 $\preceq$-规则性和强 $\preceq$-规则性问题。 4. 判定单计数器网络相关过程与确定性下推自动机相关过程之间的模拟等价性。 需要注意的是，$\preceq$-规则性问题对于一般的 Petri 网和 PA 过程是不可判定的，而单计数器自动机与确定性单计数器自动机之间的模拟等价性也是不可判定的。 #### 单计数器网络上的模拟 我们固定一个控制状态集为 $Q$ 的单计数器网络，构建集合 $S = \{ \langle p(m), q(n) \rangle : p, q \in Q, m, n \in \mathbb{N}, p(m) \preceq q(n) \}$ 的描述，即该网络关联的转换系统上的最大模拟关系。$S$ 可看作是 $|Q|^2$ 个 $\mathbb{N} \times \mathbb{N}$ 子集的集合，对于每个 $p, q \in Q$，有 $S_{\langle p,q \rangle} = \{ \langle m, n \rangle : p(m) \preceq q(n) \}$。 ##### 着色与前沿函数 我们引入着色的概念，着色 $C$ 是一个函数 $C : (Q \times Q) \to (\mathbb{N} \times \mathbb{N}) \to \{ \text{black}, \text{white} \}$，需满足单调性条件：若 $C_{\langle p,q \rangle}(m, n) = \text{black}$，则对于所有 $m' \leq m$ 和 $n' \geq n$，有 $C_{\langle p,q \rangle}(m', n') = \text{black}$。每个 $C_{\langle p,q \rangle}$ 由前沿函数 $f_{C_{\langle p,q \rangle}} : \mathbb{N} \to \mathbb{N} \cup \{ \infty \}$ 确定，定义为 $f_{C_{\langle p,q \rangle}}(n) = \min \{ m : C_{\langle p,q \rangle}(m, n) = \text{white} \}$，若对于所有 $m$ 都有 $C_{\langle p,q \rangle}(m, n) = \text{black}$，则 $f_{C_{\langle p,q \rangle}}(n) = \infty$。 我们用 $G$ 表示特定的着色： \[ G_{\langle p,q \rangle}(m, n) = \begin{cases} \text{black}, & \text{if } p(m) \preceq q(n) \\ \text{white}, & \text{if } p(m) \not\preceq q(n) \end{cases} \] $G$ 满足单调性条件，我们用 $f_{\langle p,q \rangle}$ 表示 $G_{\langle p,q \rangle}$ 的前沿函数。 ##### 带定理 带定理指出：每个前沿都位于一个具有非负有理或无穷斜率的带内。这个定理是单计数器网络模拟可判定性的核心。若前沿函数 $f$ 对于某个 $n$ 有 $f(n) = \infty$，则相应的前沿是有限的且位于水平带内；否则，$f$ 几乎是线性的，且是周期性的，即从某个 $n_0$ 开始，一个有限的步长序列会永远重复。我们可以有效计算其周期性描述，从而得到集合 $S$ 的简单描述。 ##### 前沿函数的逐步逼近 我们定义一个点 $\langle m, n \rangle$ 在着色 $C$ 中是局部正确的，当且仅当对于所有 $p, q \in Q$，若 $C_{\langle p,q \rangle}(m, n) = \text{black}$ 且 $p(m) \stackrel{a}{\to} p'(m')$，则存在 $q(n) \stackrel{a}{\to} q'(n')$ 使得 $C_{\langle p',q' \rangle}(m', n') = \text{black}$。着色 $C$ 是 $k$-可允许的，当且仅当每个 $m, n < k$ 的点 $\langle m, n \rangle$ 在 $C$ 中是局部正确的。 函数 $G_k : (Q \times Q) \to (\mathbb{N} \times \mathbb{N}) \to \{ \text{black}, \text{white} \}$ 定义为 $G_{k\langle p,q \rangle}(m, n) = \text{black}$ 当且仅当存在某个 $k$-可允许的着色 $C$ 使得 $C_{\langle p,q \rangle}(m, n) = \text{black}$。$G_k$ 是 $k$-可允许的着色，且是最大的 $k$-可允许着色，最大的 $\infty$-可允许着色 $G_{\infty}$ 显然就是 $G$。 对于 $k \in \mathbb{N}$，我们用 $f_{k\langle p,q \rangle}$ 表示 $G_{k\langle p,q \rangle}$ 的前沿函数，其值域为 $\{ 0, 1, \cdots, k - 1 \} \cup \{ \infty \}$，且对于所有 $n \geq k$，有 $f_{k\langle p,q \rangle}(n) = \infty$。每个 $f_{k\lang