9 décembre 2024
Luc Dartois (LACL)Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification.
In this talk, I will present how we can achieve efficient composition of two-way transducers, mainly through the use of Reversible Transducers. Reversible machines are machine that are both deterministic and codeterministic.
I will show how any two-way transducers can be made reversible, while being easily composable. I will also show how these results can be extended to the setting of infinite words, which is the dedicated setting for model-checking for example.