Letter-to-letter transducers are a standard formalism for modeling reactive systems. Often, two transducers that model similar systems differ locally from one another, by behaving similarly, up to permutations of the input and output letters within "rounds". In this work, we introduce and study notions of simulation by rounds and equivalence by rounds of transducers. In our setting, words are partitioned to consecutive subwords of a fixed length $k$, called rounds. Then, a transducer $\mathcal{T}_1$ is $k$-round simulated by transducer $\mathcal{T}_2$ if, intuitively, for every input word $x$, we can permute the letters within each round in $x$, such that the output of $\mathcal{T}_2$ on the permuted word is itself a permutation of the output of $\mathcal{T}_1$ on $x$. Finally, two transducers are $k$-round equivalent if they simulate each other. We solve two main decision problems, namely whether $\mathcal{T}_2$ $k$-round simulates $\mathcal{T}_1$ (1) when $k$ is given as input, and (2) for an existentially quantified $k$. We demonstrate the usefulness of the definitions by applying them to process symmetry: a setting in which a permutation in the identities of processes in a multi-process system naturally gives rise to two transducers, whose $k$-round equivalence corresponds to stability against such permutations.
翻译:逐字母转录机是建模反应式系统的标准形式化工具。通常,两个建模相似系统的转录机会在局部上存在差异:它们在"轮次"内对输入输出字母进行排列后,行为表现相似。本研究引入并探讨了转录机的轮次模拟与轮次等价概念。在我们设定的框架中,单词被分割为固定长度 $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$ 轮等价性对应于对该类置换的稳定性——我们论证了这些定义的实际效用。