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$轮等价的。我们解决了两个主要决策问题:即判断$\mathcal{T}_2$是否能$k$轮模拟$\mathcal{T}_1$:(1)当$k$作为输入给定,以及(2)存在量化的$k$。通过将定义应用于过程对称性——多进程系统中进程标识的置换自然产生两个转换器的场景,且其$k$轮等价性对应针对此类置换的稳定性——我们展示了这些定义的实用性。