Simulation by Rounds of Letter-to-Letter Transducers

TL;DR

The paper introduces k-round simulation and k-round equivalence for letter-to-letter transducers to model reactive systems under local intra-round permutations. It reduces fixed-round problems to NFAs via a trace-DFA and permutation-closure construction, establishing PSPACE membership and, for equivalence, PSPACE-hardness. For existential-round problems, it proves the existence of a finite bound $K_0$ on the round length that suffices, using Parikh vectors, Presburger arithmetic, and a redundant product automaton to achieve decidability (with a high but finite upper bound). The work connects round-based stability to process symmetry, provides a mapping-based viewpoint on witnessing simulations, and explores several symmetric variants with corresponding decidability results and open questions. Overall, the framework offers a rigorous approach to approximate simulation that preserves key behavioral properties while enabling scalable verification in symmetry-prone settings.

Abstract

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.

Figures (18)

• Figure 1: A nondeterministic automaton with one initial state $q_0$ and one accepting state $q_2$.
• Figure 2: The transducer $\mathcal{T}_i$ for RR, initial state omitted. The input letters $\sigma$ and $\lnot\sigma$ mean all letters from $2^\mathcal{P}$ that, respectively, contain or do not contain $\sigma$. The labels are written in red.
• Figure 3: Transducers $\mathcal{T}_1$ (left) and $\mathcal{T}_2$ (right) illustrate the asymmetry in the definition of round equivalence (see \ref{['example:def-asymmetric']}).
• Figure 4: A flow diagram for the proof steps in \ref{['sec:proof_of_bound']}.
• Figure 5: A diagram for the proof structure of \ref{['lem:profile_equality_to_simulation']}.

Theorems & Definitions (38)

• Example 1.1
• Example 3.1: Round-equivalence for words
• Remark 3.2: On the role of $\Lambda$
• Example 3.3: Round Robin
• Remark 3.4
• Example 3.5: Round simulation is not symmetric
• Lemma 3.6
• Lemma 4.3
• Lemma 4.4
• Remark 4.5