La programmation semi-définie est un outil fondamental d'optimisation convexe et polynomiale. Elle revient à optimiser une fonction linéaire sur un spectraèdre (un ensemble défini par des inégalités matricielles linéaires). En particulier, la programmation semi-définie est une généralisation de la programmation linéaire.Nous étudions l'analogue non-archimédien de la programmation semi-définie, en remplaçant le corps des nombres réels par le corps des séries de Puiseux. Notre approche est fondée sur des méthodes issues de la géométrie tropicale et, en particulier, sur l'étude de la tropicalisation des spectraèdres.En première partie de la thèse, nous analysons les images par la valuation des ensembles semi-algébriques généraux définis dans le corps des séries de Puiseux. Nous montrons que ces images ont une structure polyédrale, ce qui fournit un analogue réel du théorème de Bieri et Groves. Ensuite, nous introduisons la notion de spectraèdres tropicaux et nous montrons que, sous une hypothèse de généricité, ces objets sont décrits par des systèmes d'inégalités polynomiales de degré 2 sur le semi-corps tropical. Cela généralise un résultat de Yu sur la tropicalisation du cône des matrices positives.Une question importante relative à la programmation semi-définie sur les réels consiste à caractériser des projections de spectraèdres. Dans ce cadre, Helton et Nie ont conjecturé que tout ensemble semi-algébrique convexe est la projection d'un spectraèdre. La conjecture a été réfutée par Scheiderer. Néanmoins, nous montrons qu'elle est vraie ''à valuation près'' : dans le corps réel clos des séries de Puiseux, les ensembles semi-algébriques convexes et les spectraèdres projetés ont exactement les mêmes images par la valuation non-archimédienne.En seconde partie de la thèse, nous étudions des questions algorithmiques liées à la programmation semi-définie. Le problème algorithmique de base consiste à décider si un spectraèdre est vide. On ne sait pas si ce problème appartient à NP dans le modèle de la machine de Turing, et les algorithmes fondés sur la décomposition cylindrique algébrique ou la méthode de points critiques constituent l'état de l'art dans ce domaine. Nous montrons que, dans le cadre non-archimédien, les spectraèdres tropicaux génériques sont décrits par des opérateurs de Shapley associés aux jeux à paiement moyen stochastiques. Cela donne une méthode pour résoudre des problèmes de réalisabilité en programmation semi-définie non-archimédienne en utilisant les algorithmes combinatoires conçus pour les jeux stochastiques.Dans les chapitres finals de la thèse, nous établissons des bornes de complexité pour l'algorithme d'itération sur les valeurs qui exploitent la correspondance entre les jeux stochastiques et la convexité tropicale. Nous montrons que le nombre d'itérations est contrôlé par un nombre de conditionnement relié au diamètre intérieur du spectraèdre tropical associé.Nous fournissons des bornes supérieures générales sur le nombre de conditionnement. Pour cela, nous établissons des bornes optimales sur la taille en bits des mesures invariantes de chaînes de Markov. Comme corollaire, notre estimation montre que l'itération sur la valeur résout les jeux ergodiques à paiement moyen en temps pseudo-polynomial si le nombre de positions aléatoires est fixé. Enfin, nous expérimentons notre approche à la résolution de programmes semi-définis non-archimédiens aléatoires de grande taille. / Semidefinite programming (SDP) is a fundamental tool in convex and polynomial optimization. It consists in minimizing the linear functions over the spectrahedra (sets defined by linear matrix inequalities). In particular, SDP is a generalization of linear programming.The purpose of this thesis is to study the nonarchimedean analogue of SDP, replacing the field of real numbers by the field of Puiseux series. Our methods rely on tropical geometry and, in particular, on the study of tropicalization of spectrahedra.In the first part of the thesis, we analyze the images by valuation of general semialgebraic sets defined over the Puiseux series. We show that these images have a polyhedral structure, giving the real analogue of the Bieri--Groves theorem. Subsequently, we introduce the notion of tropical spectrahedra and show that, under genericity conditions, these objects can be described explicitly by systems of polynomial inequalities of degree 2 in the tropical semifield. This generalizes the result of Yu on the tropicalization of the SDP cone.One of the most important questions about real SDPs is to characterize the sets that arise as projections of spectrahedra. In this context, Helton and Nie conjectured that every semialgebraic convex set is a projected spectrahedron. This conjecture was disproved by Scheiderer. However, we show that the conjecture is true ''up to taking the valuation'': over a real closed nonarchimedean field of Puiseux series, the convex semialgebraic sets and the projections of spectrahedra have precisely the same images by the nonarchimedean valuation.In the second part of the thesis, we study the algorithmic questions related to SDP. The basic computational problem associated with SDP over real numbers is to decide whether a spectrahedron is nonempty. It is unknown whether this problem belongs to NP in the Turing machine model, and the state-of-the-art algorithms that certify the (in)feasibility of spectrahedra are based on cylindrical decomposition or the critical points method. We show that, in the nonarchimedean setting, generic tropical spectrahedra can be described by Shapley operators associated with stochastic mean payoff games. This provides a tool to solve nonarchimedean semidefinite feasibility problems using combinatorial algorithms designed for stochastic games.In the final chapters of the thesis, we provide new complexity bounds for the value iteration algorithm, exploiting the correspondence between stochastic games and tropical convexity. We show that the number of iterations needed to solve a game is controlled by a condition number, which is related to the inner radius of the associated tropical spectrahedron. We provide general upper bounds on the condition number. To this end, we establish optimal bounds on the bit-length of stationary distributions of Markov chains. As a corollary, our estimates show that value iteration can solve ergodic mean payoff games in pseudopolynomial time, provided that the number of random positions of the game is fixed. Finally, we apply our approach to large scale random nonarchimedean SDPs.

<p>Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of <i>model checking</i>. At first, we investigate two categories of problems related to model checking: <i>games</i> and <i>stochastic infinite-state systems</i>. In the end, we join these two lines of research, by studying <i>stochastic infinite-state games</i>.</p><p>Game theory has been used in verification for a long time. We focus on finite-state 2-player parity and limit-average (mean payoff) games. These problems have applications in model checking for the <i>μ</i>-calculus, one of the most expressive logics for programs. We give a simplified proof of memoryless determinacy. The proof applies <i>both</i> to parity and limit-average games. Moreover, we suggest a strategy improvement algorithm for limit-average games. The algorithm is discrete and strongly subexponential.</p><p>We also consider probabilistic infinite-state systems (Markov chains) induced by three types of models. <i>Lossy channel systems (LCS)</i> have been used to model processes that communicate over an unreliable medium. <i>Petri nets</i> model systems with unboundedly many parallel processes. <i>Noisy Turing machines</i> can model computers where the memory may be corrupted in a stochastic manner. We introduce the notion of <i>eagerness</i> and prove that all these systems are eager. We give a scheme to approximate the value of a reward function defined on paths. Eagerness allows us to prove that the scheme terminates. For probabilistic LCS, we also give an algorithm that approximates the limit-average reward. This quantity describes the long-run behavior of the system.</p><p>Finally, we investigate Büchi games on probabilistic LCS. Such games can be used to model a malicious cracker trying to break a network protocol. We give an algorithm to solve these games.</p>

Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of model checking. At first, we investigate two categories of problems related to model checking: games and stochastic infinite-state systems. In the end, we join these two lines of research, by studying stochastic infinite-state games. Game theory has been used in verification for a long time. We focus on finite-state 2-player parity and limit-average (mean payoff) games. These problems have applications in model checking for the μ-calculus, one of the most expressive logics for programs. We give a simplified proof of memoryless determinacy. The proof applies both to parity and limit-average games. Moreover, we suggest a strategy improvement algorithm for limit-average games. The algorithm is discrete and strongly subexponential. We also consider probabilistic infinite-state systems (Markov chains) induced by three types of models. Lossy channel systems (LCS) have been used to model processes that communicate over an unreliable medium. Petri nets model systems with unboundedly many parallel processes. Noisy Turing machines can model computers where the memory may be corrupted in a stochastic manner. We introduce the notion of eagerness and prove that all these systems are eager. We give a scheme to approximate the value of a reward function defined on paths. Eagerness allows us to prove that the scheme terminates. For probabilistic LCS, we also give an algorithm that approximates the limit-average reward. This quantity describes the long-run behavior of the system. Finally, we investigate Büchi games on probabilistic LCS. Such games can be used to model a malicious cracker trying to break a network protocol. We give an algorithm to solve these games.