Cette thèse de doctorat est une investigation des logiques de la connaissance, de la croyance et de la dynamique d'information, en utilisant des outils de topologie et logique épistémique (dynamique). La partie I concerne les interprétations fondées sur des preuves de croyances justifiées et connaissance. Commencer par une interprétation topologique des connaissances désormais standard en tant qu'opérateur intérieur, nous développons, de manière progressive, un cadre qui (1) peut parler de preuves non seulement sémantiquement, mais aussi le niveau syntaxique, rendant ainsi la notion de preuve plus explicite; (2) prend la preuve comme la notion la plus primitive, et définit la croyance et la connaissance purement basé sur elle. Dans la partie II de cette dissertation, nous nous concentrons sur notions de connaissances ainsi que divers types de dynamique de l'information comprenant apprendre de nouvelles preuves. Plus précisément, cette partie est centrée autour des notions de certaines connaissances et savoir-faire en tant que «connaissances potentielles», ainsi que les liens entre la notion abstraite d'effort épistémique englobant toute méthode l'acquisition de preuves et les attitudes dynamiques bien étudiées telles que les annonces publiques arbitraires. Pour résumer, cette thèse réinterprète d'une part certaines logiques épistémiques et doxastiques existantes et leurs extensions dynamiques d'un point de vue topologique, fournissant une interprétation fondée sur des preuves. D'un autre côté, elle utilise des outils topologiques pour affiner et étendre les analyses antérieures, conduisant à de nouvelles logiques de la dynamique des preuves et de l'information / This dissertation brings together epistemic logic and topology. It studies formal representations of the notion of evidence and its link to justification, justified belief, knowledge, and evidence-based information dynamics, by using tools from topology and (dynamic) epistemic logic. Part I is concerned with evidence-based interpretations of justified belief and knowledge. Starting with a by-now-standard topological interpretation of knowledge as the interior operator, we develop, in a gradual manner, a topological framework that (1) can talk about evidence not only semantically, but also at the syntactic level, thereby making the notion of evidence more explicit; (2) takes evidence as the most primitive notion, and defines belief and knowledge purely based on it, thereby linking these two crucial notions of epistemology at a deeper, more basic level. In Part II of this dissertation, we focus on notions of knowledge as well as various types of information dynamics comprising learning new evidence. More precisely, this part is centered around the notions of absolutely certain knowledge and know ability as "potential knowledge", as well as the connections between the abstract notion of epistemic effort encompassing any method of evidence acquisition and the well-studied dynamic attitudes such as public and arbitrary public announcements. To sum up, this dissertation on one hand re-interprets some existing epistemic and doxastic logics and their dynamic extensions from a topological perspective, providing an evidence-based interpretation. On the other hand, it uses topological tools to refine and extend earlier analysis, leading to novel logics of evidence and information dynamics

Nous proposons dans notre thèse une nouvelle méthodologie pour le développement des protocoles de communication et des applications réparties en explorant une approche de synthèse automatisée. Après avoir effectué un état de l'art sur les techniques de synthèse de protocoles, nous présentons, dans la première partie de la thèse, une nouvelle méthode de synthèse automatique de spécifications de protocoles à partir de spécifications de services dans un modèle de réseaux de Petri interprétés. Notre approche de synthèse est basée sur un nouveau concept de raffinement de réseaux de Petri qui assure la correction des protocoles construits de façon incrémentale. L'intérêt principal de cette méthode par rapport aux techniques classiques basées sur l'analyse est qu'elle évite la phase supplémentaire de validation du protocole qui passe souvent par une analyse exhaustive dont le problème fondamental est l'explosion combinatoire. De plus, le coût de construction des protocoles est considérablement diminué. Partant d'une description de service, notre technique de synthèse permet de dériver automatiquement au niveau protocole l'ensemble des fonctionnalités suivantes: (1) traitements répartis, (2) flot de contrôle, (3) flot de données, (4) contrôle de la cohérence des données, (5) et choix distribué. Elle constitue, de ce fait, un "bon" compromis entre le pouvoir de synthèse et le pouvoir d'expression des services relativement aux techniques existantes. Dans la deuxième partie de la thèse nous présentons une application réelle de notre méthode de synthèse à la conception du protocole de transport ISO de base (ISO 8073), le point de départ de la conception étant la spécification du service de transport ISO 8072. Dans la troisième partie de la thèse, nous présentons un ensemble d'outils logiciels pour la synthèse automatique de protocoles que nous appelons STEPS (Software Toolset for automatEd Protocol Synthesis). Nous avons développé cet ensemble d'outils afin de démontrer l'utilité et la faisabilité de l'approche de synthèse que nous proposons. La sémantique de notre modèle de spécification étant assez proche de celle du langage Estelle, nous proposons une extension de notre démarche pour la synthèse de spécifications de protocoles dans le langage Estelle. L'intérêt est que ces spécifications peuvent être directement exploitées par des outils existants afin de générer automatiquement du code exécutable ou d'effectuer des simulations et des évaluations de performances.