凯莱图自动群与可见下推自动机模型检查

### 凯莱图自动群与可见下推自动机模型检查 #### 凯莱图自动群相关内容 凯莱图自动性是群的一个重要性质，它不依赖于所选的有限生成集。也就是说，若群 $G$ 关于一个有限生成集 $S$ 是凯莱图自动的，那么它关于其他任何有限生成集也都是凯莱图自动的。 所有（双）自动群都是凯莱（双）自动的，但凯莱图自动群的范畴比自动群要广泛得多。例如，海森堡群 $H = \langle a, b | [a, [a, b]] = [b, [a, b]] = 1\rangle$ 以及许多其他非自动的幂零群都属于凯莱图自动群。并且，凯莱（双）自动群保留了（双）自动群的许多算法性质，比如每个凯莱图自动群的字问题可在二次时间内判定，每个凯莱图双自动群的共轭问题是可判定的。 凯莱图自动群具有良好的封闭性，下面这个定理很关键： 设 $A$ 和 $B$ 分别是以有限生成集 $X$ 和 $Y$ 构成的凯莱图自动群，$\tau : B \to Aut(A)$ 是一个同态，且对于 $Y$ 中的每个 $y$，自同构 $\tau(y)$ 是自动的，那么半直积 $G = A ⋊_{\tau} B$ 是凯莱图自动的。 这里解释一下凯莱图自动群 $A$ 的自动自同构 $\alpha$ 的含义。设 $A$ 在 $\Sigma$ 上是自动的，$\overline{ } : A \to \Sigma^*$ 是 $A$ 的自动结构中使用的单射。自同构 $\alpha$ 在 $A$ 上诱导出一个二元关系 $\{(a, a\alpha) | a \in A\}$，进而在 $\Sigma^*$ 上诱导出一个二元关系 $\overline{\alpha} = \{(\overline{a}, \overline{a\alpha}) | a \in A\}$。若关系 $\overline{\alpha}$ 是 $\Sigma$ 上的正则关系，则自同构 $\alpha$ 是自动的。 半直积 $A ⋊_{\tau} B$ 是所有对 $(b, a)$（其中 $b \in B$，$a \in A$）的集合，其乘积定义为 $(b_1, a_1)(b_2, a_2) = (b_1b_2, a_1^{\tau(b_2)}a_2)$。 已知有限秩的自由阿贝尔群 $A = \mathbb{Z}^d$ 和自由群 $B = F_n$ 是自动的，所以它们也是凯莱图自动的。可以证明，$\mathbb{Z}^d$ 的每个自同构都是自动的，即整数 $d$ 元组与 $GL_d(\mathbb{Z})$ 中的任何固定 $d \times d$ 矩阵的乘法是自动的。结合上述定理，能得到一些重要结论。 对于（自由 - 阿贝尔） - 自由群，当涉及共轭问题时，有如下情况。设 $C$ 是 $Aut(A) = GL_d(\mathbb{Z})$ 的一个子群，若不存在算法能判定对于 $A$ 中的任意向量对 $u$ 和 $v$，是否存在 $C$ 中的矩阵 $c$ 使得 $uc = v$，则称 $C$ 具有不可判定的轨道问题。若 $\tau : B \to GL_d(\mathbb{Z})$ 是一个同态且 $\tau(B) = C$，当 $C$ 具有不可判定的轨道问题时，半直积 $G = A ⋊_{\tau} B$ 的共轭问题是不可判定的。 可以通过特定方法构造 $GL_d(\mathbb{Z})$ 中轨道不可判定的子群。设 $d \geq 4$，$H$ 是一个具有不可判定字问题的有限表示群，利用米哈伊洛娃构造得到 $F_2 \times F_2$ 的相应有限生成子群 $H'$，其成员问题不可判定，再通过特定嵌入将 $F_2 \times F_2$ 视为 $GL_d(\mathbb{Z})$ 的子群，使得 $H$ 的字问题的不可判定性转化为 $H' = C \leq GL_d(\mathbb{Z})$ 的轨道问题的不可判定性，此时群 $G = A ⋊_{\tau} B$（其中 $\tau : B \to GL_d(\mathbb{Z})$ 是满足 $\tau(B) = C$ 的任意同态）的共轭问题是不可判定的。 上述定义的群 $C$ 是有限生成但非有限表示的，所以对于形如 $G = A ⋊_{\tau} B$ 且 $C = \tau(B)$ 的群，$\tau$ 不是单射。不过有一种改进方法，设 $C = \langle g_1, \ldots, g_n\rangle$ 是 $GL_d(\mathbb{Z})$ 中轨道不可判定的子群，$B = F(f_1, \ldots, f_n)$ 是秩为 $n$ 的自由群，$C' = \langle g_1', \ldots, g_n'\rangle$ 是 $GL_2(\mathbb{Z})$ 的任意秩为 $n$ 的自由子群，定义 $\tau : B \to GL_{d + 2}(\mathbb{Z})$ 为： $\tau(f_i) = \begin{bmatrix} g_i & 0_{d \times 2} \\ 0_{2 \times d} & g_i' \end{bmatrix}$， 其中 $0_{d \times 2}$ 和 $0_{2 \times d}$ 是适当大小的零矩阵。显然 $\tau$ 是单射，并且 $C$ 在 $GL_d(\mathbb{Z})$ 中轨道问题的不可判定性会导致自由子群 $C' = \tau(B)$ 在 $GL_{d + 2}(\mathbb{Z})$ 中轨道问题的不可判定性。 最后，那些是凯莱图自动但不是凯莱图双自动且具有不可判定共轭问题的群，在标准定义下不是自动的。实际上，相关定理表明这些例子甚至不能有次指数的德恩函数，因为标准意义下的自动群具有二次德恩函数。 #### 可见下推自动机相关内容 可见下推自动机（VPA）是一种特殊的下推自动机，其栈行为（即执行压栈、弹栈或不进行栈操作）完全由输入符号根据输入字母表的固定划分决定。每个非确定性 VPA 都可以转换为等价的确定性 VPA，这使得检查下推模型的上下文无关属性在调用和返回可见的情况下是可判定的。可见下推自动机在处理 XML 流、组件系统的 AOP 协议等方面很有用。 检查非确定性 VPA $M$ 的普遍性（即检查 $L(M) = \Sigma^*$）的标准方法是先使其完备，再确定化、求补，最后检查是否为空。检查包含问题 $L(M) \subseteq L(N)$ 的标准方法是计算 $N$ 的补集，与 $M$ 取交集，然后检查是否为空。但这些方法成本高，因为计算补集需要完全确定化，而 VPA 的确定化需要指数时间的膨胀。 为了解决这个问题，提出了优化的即时算法。首先是普遍性检查： - **标准方法**：先确定化自动机，然后检查非接受状态的可达性。使用 P - 自动机技术计算确定化 VPA 的可达配置。若找到拒绝配置，则原 VPA 不是普遍的；若所有可达配置都是接受的，则原 VPA 是普遍的。 - **优化的即时方法**：同时进行即时确定化和 P - 自动机的构建。有两个交错的阶段，先逐步确定化 VPA $M$，每次确定化后更新 P - 自动机；然后使用 P - 自动机再次进行确定化。该过程会终止，因为 $M_{od}$ 的大小是有限的，P - 自动机的构建也会终止。通过定义状态和栈符号的偏序关系，只计算最小可达配置并检查是否存在拒绝配置。 下面是相关算法： ```plaintext Algorithm 1. Optimized determinization for VPA Data: A nondeterministic VPA M = (Q, Γ, Q0, Δ, F) Result: A determinized VPA M od = (Q′, Γ ′, Q′ 0, Δ′, F ′) 1 begin 2 Q′ = 2Q×Q, Γ ′ = Q′ × Σc, 3 Q′ 0 = {IdQ0}, F ′ = {S ∈Q′ | Π2(S) ∩F ̸= ∅}, 4 and the transition relation Δ′ = Δ′ i ∪Δ′ c ∪Δ′ r is given by: – Internal: For ever ```