Sur les problèmes de décision concernant les transducteurs de mots avec la sémantique d'origine

Abstract

La sémantique d'origine pour les transducteurs de mots a été introduite par Bojańczyk en 2014 afin d'obtenir une caractérisation indépendante de la machine pour les fonctions mot à mot définies par les transducteurs. Notre objectif principal était d'étudier certains problèmes de décision classiques pour les transducteurs dans la sémantique d'origine, tels que le problème d'inclusion et d'équivalence. Nous avons montré que ces problèmes deviennent décidables dans la sémantique d'origine, même si la version classique est indécidable.Motivé par l'observation que la sémantique d'origine est plus fine que la sémantique classique, nous avons défini les resynchroniseurs comme un moyen de décrire les distorsions d'origine et d'étudier les problèmes ci-dessus de manière relaxée. Nous avons étendu le modèle des resynchroniseurs rationnels, introduit par Filiot et al. pour les transducteurs unidirectionnels, aux resynchroniseurs réguliers, qui fonctionnent pour des classes de transducteurs plus grandes.Nous avons étudié les deux variantes du problème d’inclusion relative à une resynchronisation, qui demande si un transducteur est contenu dans un autre jusqu'à une distorsion spécifiée par un resynchroniseur. Nous avons montré que le problème peut être résolu lorsque le resynchroniseur fait partie de l'entrée. Lorsque le resynchroniseur n'est pas spécifié dans l'entrée, nous avons cherché à synthétiser un tel resynchroniseur, chaque fois que cela était possible. Nous appelons cela le problème de synthèse pour les resynchroniseurs et nous montrons qu'il est indécidable en général. Nous avons identifié quelques cas restreints où le problème devient décidable. Nous avons également étudié le problème de resynchronisabilité unidirectionnelle, qui demande si un transducteur bidirectionnel donné est resynchronisable dans un transducteur unidirectionnel, et nous avons montré que ce problème est également décidable.