Dans le cadre de la télécommunication, les entreprises développent des protocoles gérant le transfert de données entre machines. Ces protocoles fonctionnent sur le principe d'envoi de messages entre deux parties par l'intermédiaire de canaux non fiables. Pour s'assurer que tous les messages ont bien été reçus, les techniques employées consistent à réémettre les messages perdus et/ou à attendre un laps de temps déterminé avant de conclure à l'échec de la transmission. De plus, les systèmes sont souvent modélisés en fonction de paramètres. Nous avons travaillé sur un modèle mathématique permettant la vérification de spécifications (comportements attendus des systèmes) pour des protocoles manipulant à la fois des compteurs, des files d'attente ou des horloges, ainsi que des paramètres. Le but de l'analyse est de calculer l'ensemble des comportements possibles du système puis de vérifier qu'aucun d'eux ne viole une spécification attendue. Le problème ici est que cet ensemble est infini. En effet, un comportement est fonction des valeurs prises par les variables du système au cours de l'exécution et certaines sont définies sur un domaine infini. Il faut alors pouvoir représenter ces comportements de façon finie et aussi trouver des méthodes pour calculer en un temps fini un ensemble infini. Plus formellement, nous nous sommes placés dans le cadre de l'analyse automatique des systèmes (model-checking). La représentation choisie pour les modèles à compteurs et horloges paramétrés est une extension des matrices de bornes pour laquelle nous avons une méthode exacte d'accélération (calcul en un temps fini d'ensembles de comportements infinis). Du côté pratique, nous avons implanté ces méthodes dans un outil TReX qui est, à notre connaissance, le seul pouvant manipuler de manière exacte des compteurs, des horloges et des files d'attente. Nous avons pu vérifier des exemples conséquents tels que le protocole de retransmission bornée.

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 / In this thesis, we study classes of infinite graphs and their properties,especially the model-checking problem, the accessibility problem and therecognised languages.We define a notion of stack trees, and a related notionof ground rewriting, which is an extension of both higher-order pushdownautomata and ground tree rewriting systems. We also define a notion ofrecognisability on the sets of ground rewriting operations through operationautomata. This notion induces a notion of recognisability over sets of stacktrees and a normalisation of recognisable sets of operations, similar to theknown notions over higher-order pushdown automata. We show that the graphsdefined by these ground stack tree rewriting systems have a decidableFO-theory, by exhibiting a finite set interpretation from a graph defined bya higher-order automaton to a graph defined by a ground stack tree rewritingsystem.We also consider the context-freeness problem for counter systems, andthe related problem of stratifiability of semi-linear sets. We prove thedecidability of the stratifiability problem for integral polyhedra and that itis coNP-complete. We use this result to show that the context-freeness problemfor flat counter systems is as well coNP-complete. Finally, we give a new proofof the decidability of the context-freeness problem for vector additionsystems, previously studied by Schwer

L'un des aspects fondamentaux des systèmes informatiques modernes, et en particulier des systèmes critiques, est la possibilité d'exécuter plusieurs processus, partageant des ressources communes, de façon simultanée. De par leur nature concurrentielle, le bon fonctionnement de ces systèmes n'est assuré que lorsque leurs comportements ne dépendent pas d'un ordre d'exécution prédéterminé. En raison de cette caractéristique, il est particulièrement difficile de s'assurer qu'un système concurrent ne possède pas de faille. Dans cette thèse, nous étudions la vérification formelle, une approche algorithmique qui vise à automatiser la vérification du bon fonctionnement de systèmes concurrents en procédant par une abstraction vers des modèles mathématiques. Nous considérons deux de ces modèles, les réseaux de Petri et les systèmes d'addition de vecteurs, et les problèmes de vérification qui leur sont associés. Nous montrons que le problème d'accessibilité pour les systèmes d'addition de vecteurs (avec états) à deux compteurs est PSPACE-complet, c'est-à-dire complet pour la classe des problèmes solubles à l'aide d'une quantité polynomiale de mémoire. Nous établissons ainsi la complexité calculatoire précise de ce problème, répondant à une question demeurée ouverte depuis plus de trente ans. Nous proposons une nouvelle approche au problème de couverture pour les réseaux de Petri, basée sur un algorithme arrière guidé par une caractérisation logique de l'accessibilité dans les réseaux de Petri dits continus. Cette approche nous a permis de mettre au point un nouvel algorithme qui s'avère particulièrement efficace en pratique, tel que démontré par notre implémentation logicielle nommée QCover. Nous complétons ces résultats par une étude des systèmes de transitions bien structurés qui constituent une abstraction générale des systèmes d'addition de vecteurs et des réseaux de Petri. Nous considérons le cas des systèmes de transitions bien structurés à branchement infini, une classe qui inclut les réseaux de Petri possédant des arcs pouvant consommer ou produire un nombre arbitraire de jetons. Nous développons des outils mathématiques facilitant l'étude de ces systèmes et nous délimitons les frontières au-delà desquelles la décidabilité des problèmes de terminaison, de finitude, de maintenabilité et de couverture est perdue. / One fundamental aspect of computer systems, and in particular of critical systsems, is the ability to run simultaneously many processes sharing resources. Such concurrent systems only work correctly when their behaviours are independent of any execution ordering. For this reason, it is particularly difficult to ensure the correctness of concurrent systems.In this thesis, we study formal verification, an algorithmic approach to the verification of concurrent systems based on mathematical modeling. We consider two of the most prominent models, Petri nets and vector addition systems, and their usual verification problems considered in the literature.We show that the reachability problem for vector addition systems (with states) restricted to two counters is PSPACE-complete, that is, it is complete for the class of problems solvable with a polynomial amount of memory. Hence, we establish the precise computational complexity of this problem, left open for more than thirty years.We develop a new approach to the coverability problem for Petri nets which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. We demonstrate the effectiveness of our approach by implementing it in a tool named QCover.We complement these results with a study of well-structured transition systems which form a general abstraction of vector addition systems and Petri nets. We consider infinitely branching well-structured transition systems, a class that includes Petri nets with special transitions that may consume or produce arbitrarily many tokens. We develop mathematical tools in order to study these systems and we delineate the decidability frontier for the termination, boundedness, maintainability and coverability problems for these systems.