Skip to Main content Skip to Navigation
Theses

Réécriture d’arbres de piles et traces de systèmes à compteurs

Résumé : Dans cette thèse, nous nous attachons à étudier des classes de graphes infinis et leurs propriétés, Notamment celles de vérification de modèles, d'accessibilité et de langages reconnus.Nous définissons une notion d'arbres de piles ainsi qu'une notion liée de réécriture suffixe, permettant d'étendre à la fois les automates à piles d'ordre supérieur et la réécriture suffixe d'arbres de manière minimale. Nous définissons également une notion de reconnaissabilité sur les ensembles d'opérations à l'aide d'automates qui induit une notion de reconnaissabilité sur les ensembles d'arbres de piles et une notion de normalisation des ensembles reconnaissables d'opérations analogues à celles existant sur les automates à pile d'ordre supérieur. Nous montrons que les graphes définis par ces systèmes de réécriture suffixe d'arbres de piles possèdent une FO-théorie décidable, en montrant que ces graphes peuvent être obtenu par une interprétation à ensembles finis depuis un graphe de la hiérarchie à piles.Nous nous intéressons également au problème d'algébricité des langages de traces des systèmes à compteurs et au problème lié de la stratifiabilité d'un ensemble semi-linéaire. Nous montrons que dans le cas des polyèdres d'entiers, le problème de stratifiabilité est décidable et possède une complexité coNP-complète. Ce résultat nous permet ensuite de montrer que le problème d'algébricité des traces de systèmes à compteurs plats est décidable et coNP-complet. Nous donnons également une nouvelle preuve de la décidabilité des langages de traces des systèmes d'addition de vecteurs, préalablement étudié par Schwer
Document type :
Theses
Complete list of metadatas

https://pastel.archives-ouvertes.fr/tel-01286343
Contributor : Abes Star :  Contact
Submitted on : Thursday, March 10, 2016 - 4:15:38 PM
Last modification on : Wednesday, February 26, 2020 - 7:06:07 PM

File

TH2015PESC1122_diffusion.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01286343, version 1

Citation

Vincent Penelle. Réécriture d’arbres de piles et traces de systèmes à compteurs. Informatique et langage [cs.CL]. Université Paris-Est, 2015. Français. ⟨NNT : 2015PESC1122⟩. ⟨tel-01286343⟩

Share

Metrics

Record views

245

Files downloads

140