On Post’s embedding problem and the complexity of lossy channels

• Main Author: Chambart, Pierre
• Other Authors: Cachan, Ecole normale supérieure
• Language: en
• Published: 2011
• Subjects: Systèmes à canaux non fiables; Vérification formelle; Lossy channel systems; Model-checking; Multiply recursive function; Post's embedding problem
• Online Access: http://www.theses.fr/2011DENS0036/document

Les systèmes à canaux non fiables ont été introduits à l'origine comme un modèle de communication. Ils ont donné naissance à une classe de complexité restée mal comprise pendant longtemps. Dans cette thèse, nous étudions et comblons certaines des plus importantes lacunes dans la connaissance de cette classe. Nous fournissons entre autres des bornes inférieure et supérieure qui se rejoignent pour la complexité en temps. Puis nous proposons un nouvel outil de preuve : le Problème de Sous Mot de Post (PEP). C'est un problème simple, inspiré du Problème de Correspondance de Post, et complet pour cette classe de complexité. Nous étudions ensuite PEP et ses variantes, ainsi que les langages de solutions de PEP sur lesquels nous avons fourni des résultats de complexité et des outils de preuve tels que des lemmes de pompage. === Lossy channel systems were originally introduced to model communication protocols. It gave birth to a complexity class wich remained scarcely undersood for a long time. In this thesis we study some of the most important gaps. In particular, we bring matching upper and lower bounds for the time complexity. Then we describe a new proof tool : the Post Embedding Problem (PEP) which is a simple problem, closely related to the Post Correspondence Problem, and complete for this complexity class. Finally, we study PEP, its variants and the languages of solutions of PEP on which we provide complexity results and proof tools like pumping lemmas.