Simulation by Rounds of Letter-To-Letter Transducers

Authors Antonio Abu Nassar, Shaull Almagor

Thumbnail PDF


  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Antonio Abu Nassar
  • Computer Science Department, Technion, Haifa, Israel
Shaull Almagor
  • Computer Science Department, Technion, Haifa, Israel

Cite AsGet BibTex

Antonio Abu Nassar and Shaull Almagor. Simulation by Rounds of Letter-To-Letter Transducers. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik (2022)


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 𝒯₁ is k-round simulated by transducer 𝒯₂ if, intuitively, for every input word x, we can permute the letters within each round in x, such that the output of 𝒯₂ on the permuted word is itself a permutation of the output of 𝒯₁ on x. Finally, two transducers are k-round equivalent if they simulate each other. We solve two main decision problems, namely whether 𝒯₂ k-round simulates 𝒯₁ (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.

Subject Classification

ACM Subject Classification
  • Theory of computation β†’ Verification by model checking
  • Theory of computation β†’ Concurrency
  • Theory of computation β†’ Abstraction
  • Transducers
  • Permutations
  • Parikh
  • Simulation
  • Equivalence


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. S. Almagor. Process symmetry in probabilistic transducers. In 40th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2020, 2020. Google Scholar
  2. R. Alur. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, 2010. Google Scholar
  3. I. Borosh and L. B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. Google Scholar
  4. J. A. Brzozowski and I. Simon. Characterizations of locally testable events. Discrete Mathematics, 4(3):243-271, 1973. Google Scholar
  5. P. J. Cameron et al. Permutation groups, volume 45. Cambridge University Press, 1999. Google Scholar
  6. E. M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. Formal methods in system design, 9(1-2):77-104, 1996. Google Scholar
  7. E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  8. D. C Cooper. Theorem proving in arithmetic without multiplication. Machine intelligence, 7(91-99):300, 1972. Google Scholar
  9. E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal methods in system design, 9(1-2):105-131, 1996. Google Scholar
  10. H. Fernau, M. Paramasivan, and M. L. Schmid. Jumping finite automata: characterizations and complexity. In International Conference on Implementation and Application of Automata, pages 89-101. Springer, 2015. Google Scholar
  11. M.J. Fischer and M.O. Rabin. Super-exponential Complexity of Presburger Arithmetic. Project MAC: MAC technical memorandum. Massachusetts Institute of Technology Project MAC, 1974. URL:
  12. C. Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL:
  13. T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. 8th Conferance on Concurrency Theory, volume 1243 of Lecture Notes in Computer Science, Warsaw, July 1997. Springer-Verlag. Google Scholar
  14. M. P. Herlihy and J. M. Wing. Axioms for concurrent objects. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 13-26, 1987. Google Scholar
  15. S. Hoffmann. State complexity bounds for the commutative closure of group languages. In International Conference on Descriptional Complexity of Formal Systems, pages 64-77. Springer, 2020. Google Scholar
  16. C. N. Ip and D. L. Dill. Better verification through symmetry. Formal methods in system design, 9(1-2):41-75, 1996. Google Scholar
  17. A. W. Lin, T. K. Nguyen, P. RΓΌmmer, and J. Sun. Regular symmetry patterns. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 455-475. Springer, 2016. Google Scholar
  18. A. Meduna and P. Zemek. Jumping finite automata. International Journal of Foundations of Computer Science, 23(07):1555-1578, 2012. Google Scholar
  19. R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pages 481-489. British Computer Society, 1971. Google Scholar
  20. D. C. Oppen. A 222pn upper bound on the complexity of presburger arithmetic. Journal of Computer and System Sciences, 16(3):323-332, 1978. Google Scholar
  21. R. J. Parikh. On context-free languages. J. of the ACM, 13(4):570-581, 1966. Google Scholar
  22. K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational horn clauses. In International Conference on Automated Deduction, pages 337-352. Springer, 2005. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail