字母到字母转换器的按轮模拟

字母到字母转换器是建模反应系统的标准形式化工具。常常，两个建模相似系统的转换器彼此局部不同，表现为在“轮”内对输入与输出字母进行置换后行为相似。本工作中，我们引入并研究转换器的按轮模拟与按轮等价概念。在我们的设定中，词被划分为固定长度 $k$ 的连续子词，称为轮。直观上，若对任意输入词 $x$，我们可在 $x$ 的每轮内置换字母，使得转换器 $\mathcal{T}_2$ 在置换后词上的输出本身是转换器 $\mathcal{T}_1$ 在 $x$ 上输出的一个置换，则称转换器 $\mathcal{T}_1$ 被转换器 $\mathcal{T}_2$ $k$-轮模拟。最后，若两个转换器相互模拟，则称它们 $k$-轮等价。我们解决两个主要判定问题，即 (1) 当 $k$ 作为输入给定时，$\mathcal{T}_2$ 是否 $k$-轮模拟 $\mathcal{T}_1$；以及 (2) 对存在量词限定的 $k$ 是否成立。我们通过将定义应用于进程对称性来展示其实用性：在该设定中，多进程系统里进程标识的置换自然产生两个转换器，其 $k$-轮等价对应于对此类置换的稳定性。