Antonio Abu Nassar ; Shaull Almagor - Simulation by Rounds of Letter-to-Letter Transducers

lmcs:9920 - Logical Methods in Computer Science, December 5, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:19)2023
Simulation by Rounds of Letter-to-Letter TransducersArticle

Authors: Antonio Abu Nassar ; Shaull Almagor

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.


Volume: Volume 19, Issue 4
Secondary volumes: Selected Papers of the 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Published on: December 5, 2023
Accepted on: September 5, 2023
Submitted on: August 16, 2022
Keywords: Computer Science - Formal Languages and Automata Theory, Computer Science - Logic in Computer Science
Funding:
    Source : OpenAIRE Graph
  • Devising certifiable and explainable algorithms for verification and planning in cyber-physical systems; Funder: European Commission; Code: 837327

1 Document citing this article

Consultation statistics

This page has been seen 1864 times.
This article's PDF has been downloaded 504 times.