Un système distribué est un système composé d'éléments de calcul autonomes dotés de capacité de communication. Il s'agit d'un modèle commun pour l'étude des réseaux. L'évolution rapide des réseaux sans fils et/ou mobiles aussi bien dans la vie quotidienne que dans la recherche amène progressivement à intégrer la dynamique (i.e. l'évolution dans le temps de la connectivité) dans les systèmes distribués. Concrètement, cela revient à ajouter l'hypothèse que les capacités de communication des éléments du système peuvent varier dans le temps. De nombreux modèles considèrent ainsi la dynamique comme composante à part entière du système (et non pas comme une faute). De manière récente, une nouvelle approche, appelée graphe variant dans le temps, tente d'unifier tous ces modèles dans un formalisme commun qui permet de classifier les systèmes en fonction de leurs propriétés de connexité temporelle. Dans cette thèse, nous nous intéressons à des systèmes distribués hautement dynamiques dans lesquels les hypothèses de connexité sont minimalistes. Plus précisément, nous concentrons nos efforts sur les systèmes connexes à travers le temps dans lesquels la seule garantie est que tout élément du système peut infiniment souvent envoyer un message à tout autre (sans garantie sur la pérennité de la route utilisée ni sur le délai de communication). Nous nous intéressons plus particulièrement aux problèmes de couverture (par exemple, ensemble dominant minimal, couplage maximal, ensemble indépendant maximal, ...) dans ces systèmes distribués hautement dynamiques. Les contributions de cette thèse dans ce contexte sont les suivantes. Nous proposons tout d'abord une nouvelle définition pour les problèmes de couverture qui est plus adaptée aux systèmes distribués hautement dynamiques que les définitions existantes. Dans un deuxième temps, nous fournissons un outil générique qui permet de faciliter les preuves de résultats d'impossibilité dans les systèmes distribués dynamiques. Nous appliquons cet outil pour prouver plusieurs résultats d'impossibilité à propos de problèmes de couverture. Ensuite, nous proposons une nouvelle mesure de complexité en temps qui permet de comparer équitablement les performances de protocoles dans les systèmes distribués dynamiques. Enfin, nous donnons un algorithme de construction d'un ensemble dominant minimal dans les systèmes distribués hautement dynamiques. / A distributed system is a system of autonomous computing components endowed with communication abilities. This is a common model for the study of networks. The quick evolution of wireless and mobile network both in everyday life and in research gradually leads to take in account the dynamics (i.e. the evolution over time) in distributed systems. Concretely, this means to add the assumption that the communication abilities of the components of the system may vary over time. Many models consider the dynamics as an integral component of the system (and not as a fault). Recently, a new approach, called time-varying graph, attempts to unify all these models in a common formalism which allows the classification systems based on their temporal connectivity properties. In this thesis, we are interested in highly dynamic distributed systems with minimal connectivity assumptions. Specifically, we focus on connected over time systems where the only guarantee is that any element of the system can infinitely often send a message to any other (no guarantee are provided on the sustainability of the used path nor on the time communication). We are particularly interested in covering problems (e.g., minimal dominanting set, maximal matching, maximal independent set, ...) in these highly dynamic distributed systems. The contributions of this thesis in this context are as follows. We first propose a new definition for the covering problems which is more suited to highly dynamic distributed systems that the existing definitions. Secondly, we provide a generic tool to simplify proof of impossibility results in dynamic distributed systems. We use this tool to prove some impossibility results of covering problems. Then, we propose a new time complexity measure to fairly compare the algorithms performance in dynamic distributed systems. Finally, we give an algorithm that compute a minimal dominating set in highly dynamic distributed systems.

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay / 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 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 systems, 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.