Le model checking est une technique établie pour vérifier automatiquement qu’un modèle vérifie une propriété temporelle donnée. Lorsque le modèle viole la propriété, le model checker retourne un contre-exemple, i.e., une séquence d’actions menant à un état où la propriété n’est pas satisfaite. Comprendre ce contre-exemple pour le débogage de la spécification est une tâche compliquée pour plusieurs raisons: (i) le contre-exemple peut contenir un grand nombre d’actions; (ii) la tâche de débogage est principalement réalisée manuellement; (iii) le contre-exemple n’indique pas explicitement la source du bogue qui est caché dans le modèle; (iv) les actions les plus pertinentes ne sont pas mises en évidence dans le contre-exemple; (v) le contre-exemple ne donne pas une vue globale du problème.Ce travail présente une nouvelle approche qui rend plus accessible le model checking en simplifiant la compréhension des contre-exemples. Notre solution vise à ne garder que des actions dans des contre-exemples pertinents à des fins de débogage. Pour y parvenir, on détecte dans les modèles des choix spécifiques entre les transitions conduisant à un comportement correct ou à une partie du modèle erroné. Ces choix, que nous appelons neighbourhoods, se révèlent être de grande importance pour la compréhension du bogue à travers le contre-exemple. Pour extraire de tels choix, nous proposons deux méthodes différentes. La première méthode concerne le débogage des contre-exemples pour la violations de propriétés de sûreté. Pour ce faire, elle construit un nouveau modèle de l’original contenant tous les contre-exemples, puis compare les deux modèles pour identifier les neighbourhoods. La deuxième méthode concerne le débogage des contre-exemples pour la violations de propriétés de vivacité. À partir d’une propriété de vivacité, elle étend le modèle avec des informations de préfixe / suffixe correspondants à cette propriété. Ce modèle enrichi est ensuite analysé pour identifier les neighbourhoods.Un modèle annoté avec les neighbourhoods peut être exploité de deux manières. Tout d’abord, la partie erronée du modèle peut être visualisée en se focalisant sur les neighbourhoods, afin d’avoir une vue globale du comportement du bogue. Deuxièmement, un ensemble de techniques d’abstraction que nous avons développées peut être utilisé pour extraire les actions plus pertinentes à partir de contre-exemples, ce qui facilite leur compréhension. Notre approche est entièrement automatisée par un outil que nous avons implémenté et qui a été validé sur des études de cas réels dans différents domaines d’application. / Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain a large number of actions; (ii) the debugging task is mostly achieved manually; (iii) the counterexample does not explicitly point out the source of the bug that is hidden in the model; (iv) the most relevant actions are not highlighted in the counterexample; (v) the counterexample does not give a global view of the problem.This work presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. This is achieved by detecting in the models some specific choices between transitions leading to a correct behaviour or falling into an erroneous part of the model. These choices, which we call "neighbourhoods", turn out to be of major importance for the understanding of the bug behind the counterexample. To extract such choices we propose two different methods. One method aims at supporting the debugging of counterexamples for safety properties violations. To do so, it builds a new model from the original one containing all the counterexamples, and then compares the two models to identify neighbourhoods. The other method supports the debugging of counterexamples for liveness properties violations. Given a liveness property, it extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify neighbourhoods.A model annotated with neighbourhoods can be exploited in two ways. First, the erroneous part of the model can be visualized with a specific focus on neighbourhoods, in order to have a global view of the bug behaviour. Second, a set of abstraction techniques we developed can be used to extract relevant actions from counterexamples, which makes easier their comprehension. Our approach is fully automated by a tool we implemented and that has been validated on real-world case studies from various application areas.

Cette étude porte sur les problèmes d'apprentissage de la démonstration en mathématique dans le premier cycle de l'enseignement secondaire. Le cadre théorique a été élaboré à partir de la théorie des situations didactiques au sens de Brousseau et du modèle de Lokatos de la didactique des preuves et des réfutations

Nous étudions des méthodes de recherche simultanée de refutation et de modèle. Nous proposons une méthode pour la construction de modèles finis réduisant de façon importante l'espace de recherche des approches existantes. Nous nous intéressons ensuite à la recherche de modèles infinis. Nous étendons les méthodes RAMC (Refutation And Model Construction) et RAMCET (Refutation And Model Construction with Equational Tableaux) définie par R. Caferra et N. Zabel en introduisant de nouvelles règles et stratégies. Ces extensions augmentent strictement les capacités de la méthode, à la fois pour la recherche de preuve et de contre-exemple. Nous montrons que les méthodes proposées sont des procédures de décision uniforme pour une large clase de formules logiques. Ensuite, nous proposons et étudions de nouveaux formalismes pour représenter les modèles: les termes avec exposants entiers et les automates d'arbres. Nous prouvons la décidabilité de la théorie du premier ordre sur les termes avec exposants. Nous proposons également une nouvelle approche pour la découverte et l'utilisation de l'analogie en recherche simultanée de preuve et de contre-exemple et nous montrons comment utiliser la méthode RAMC en Programmation Logique (pour étendre les capacités des interpréteurs, détecter, voire corriger des erreurs dans les programmes etc.). Enfin, nous décrivons le système RAMC-ATINF implémentant certaines des idées proposées et nous donnons quelques résultats expérimentaux.

Dans cette thèse nous donnons une description complète de la dynamique d'une classe L de fonctions de degré un du cercle, supposées de classe (deux fois dérivable) C^2 à l'exception de deux points où seule la continuité est exigée, et telles qu'elles soient constantes sur un des intervalles délimité par ces derniers. De plus sur des demi-voisinages ouverts de ces points elles s'écrivent sous la forme x^l où l est un nombre réel positif appelé l'exposant critique de la fonction. Dans le chapitre 2 nous montrons pour la sous-classe de L des fonctions dont le nombre de rotation est de type borné, l'existence d'une transition dans la géométrie du système lorsque l'exposant critique traverse 2. Le cas plus général de fonctions en L avec nombre de rotation infinie est considéré dans le chapitre 3. Il devient pourtant plus délicat d'émettre des conjectures ; on rencontre parfois des surprises dues à laprésence de phénomènes paraboliques. De plus, nos résultats sur les applications du cercle nous permettent d'étudier l'intéressante théorie des flots de Cherry (chapitre 4). En particulier, on construit un exemple de tel flot qui a ensemble quasi-minimale métriquement non trivial. Nous donnons également une description complète des mesures physiques sur ce flot. Dans le chapitre 5 nous construisons un contrexemple de Denjoy qui est un difféomorphisme (indéfiniment dérivable) C^∞ partout sauf dans un point qui est demi-critique plat pour la fonction.

Avec la montée de la connectivité entre les appareils (internet des objets), nouvelles possibilités de coordination entre les différentes entités ont ouvert. En même temps, des résultats récents, issus de la théorie de l'information, ont fourni des limites pour la performance optimale que tout système de coordination pourrait atteindre sous certaines structures d'information. Dans cette thèse, nous développons ces résultats théoriques dans le but de les rendre plus facilement applicable aux problèmes pratiques. À cet égard, la contribution de cette thèse est double : 1) En outre développer les résultats théoriques pour fournir un aperçu de la structure des solutions au problème d'optimisation posés dans les travaux antérieurs, ainsi que la généralisation des résultats. 2) Développer des algorithmes qui exploitent le cadre théorique fourni par les travaux antérieurs pour concevoir des mécanismes de coordination pratiques, décentralisées et robustes. La généralité de l'approche se prête à diverses applications, dont les éléments suivants ont été traités: optimisation de puissance dans les réseaux sans fil, planification de la consommation d'énergie dans les applications de réseau intelligent, ainsi que Witsenhausen contre-exemple, un problème important issu de la théorie du contrôle. Diverses possibilités sont encore à venir pour exploiter le cadre et les outils développés ici. En effet, ils pourraient être utiles même dans des domaines qui ne sont pas abordés dans cette thèse, mais qui nécessitent une coordination entre les agents avec des informations différentes à la disposition de chacun. / With the rise in connectivity between appliances (Internet of Things), new avenues for coordination between various entities have opened up. At the same time, recent information theoretical results have provided bounds for the performance that any coordination scheme could achieve under certain information structures. In this thesis, we further develop those information theoretical results with the aim of making them applicable more easily to practical problems. In this regard, the contribution of this thesis is twofold: 1) Further developing the aforementioned information theoretical results to provide insights into the structure of the solutions to optimization problem posed in them, as well as generalizing some results. 2) Developing algorithms which exploit the theoretical framework provided by Information theory to devise practical, decentralized and robust coordination schemes. The generality of the approach lends itself to various applications, of which the following were treated: power optimization in wireless networks, power consumption scheduling in smart grid applications, as well as Witsenhausen counterexample, an important toy problem in control theory. Various opportunities still lie ahead to exploit the framework and tools developed herein. Indeed, they could be useful even in domains which have not been explored in this thesis but which require coordination between agents with different information available to each.

Dans cette thèse nous donnons une description complète de la dynamique d’une classe L de fonctions de degré un du cercle, supposées de classe (deux fois dérivable) C^2 à l’exception de deux points où seule la continuité est exigée, et telles qu’elles soient constantes sur un des intervalles délimité par ces derniers. De plus sur des demi-voisinages ouverts de ces points elles s’écrivent sous la forme x^l où l est un nombre réel positif appelé l’exposant critique de la fonction. Dans le chapitre 2 nous montrons pour la sous-classe de L des fonctions dont le nombre de rotation est de type borné, l’existence d’une transition dans la géométrie du système lorsque l’exposant critique traverse 2. Le cas plus général de fonctions en L avec nombre de rotation infinie est considéré dans le chapitre 3. Il devient pourtant plus délicat d’émettre des conjectures ; on rencontre parfois des surprises dues à laprésence de phénomènes paraboliques. De plus, nos résultats sur les applications du cercle nous permettent d’étudier l’intéressante théorie des flots de Cherry (chapitre 4). En particulier, on construit un exemple de tel flot qui a ensemble quasi-minimale métriquement non trivial. Nous donnons également une description complète des mesures physiques sur ce flot. Dans le chapitre 5 nous construisons un contrexemple de Denjoy qui est un difféomorphisme (indéfiniment dérivable) C^∞ partout sauf dans un point qui est demi-critique plat pour la fonction. / The principal purpose of this thesis is to give a complete description of the dynamics of a class L of circle maps of degree one, supposed to be (two times differentiable) C^2 everywhere with the exception of two points where the maps are continuous. Moreover the maps are constant on any of the two intervals delimited by this two points. In particular, on a half open neighborhood of this two points the maps can be written as an x^l where the real positive number l is called the critical exponent of the function. In Chapter 2 we prove the existence of a global phase transition when the critical exponent passes through l = 2, for functions of L with rotation number of bounded type. The more general case of function in L with rotation number of unbounded type is studied in Chapter 3. In this case it becomes more delicate to make conjectures ; in fact it often hides surprises due to the presence of underlying parabolic phenomena. Moreover, our results on circle maps give us the opportunity to study the interesting theory of Cherry flows (Chapter 4). In particular we construct an example of such a flow with a metrically non-trivial quasi-minimal set and we give a complete description on the physical measures for this kind of flows. In Chapter 5 we construct a Denjoy counterexample which is a (smooth) C^∞ diffeomorphism away from a half-critical point.