Simulation by Rounds of Letter-to-Letter Transducers

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Nassar, Antonio Abu, Almagor, Shaull
Format: Preprint
Publié: 2021
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866909103559802880
author Nassar, Antonio Abu
Almagor, Shaull
author_facet Nassar, Antonio Abu
Almagor, Shaull
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2105_01512
institution arXiv
publishDate 2021
record_format arxiv
spellingShingle Simulation by Rounds of Letter-to-Letter Transducers
Nassar, Antonio Abu
Almagor, Shaull
Formal Languages and Automata Theory
Logic in Computer Science
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.
title Simulation by Rounds of Letter-to-Letter Transducers
topic Formal Languages and Automata Theory
Logic in Computer Science
url https://arxiv.org/abs/2105.01512