I will defend my thesis on Friday 29th November, 2019, at 10:00 in the Condorcet room located on the first floor of d'Alembert building, at the ENS Paris-Saclay. It will be followed by the traditional "pot de thèse" at the Condorcet space.
Within the research community, there is a great interest in exploring many applications of energy networks since these become more and more important in our modern world. To properly design and implement these networks, advanced and complex mathematical tools are necessary. Two key features for their design are correctness and optimality. While these last two properties are in the core of formal methods, their effective application to energy networks remains largely unexploited. This constitutes one strong motivation for the work developed in this thesis. A special emphasis is made on the generic problem of power consumption scheduling. This is a scenario in which the consumers have a certain energy demand and want to have this demand to be fulfilled before a set deadline (e.g., an Electric Vehicle (EV) has to be recharged within a given time window set by the EV owner). Therefore, each consumer has to choose at each time the consumption power so that the final accumulated energy reaches a desired level. The way in which the power levels are chosen is according to a "strategy" mapping at any time the relevant information of a consumer (e.g., the current accumulated energy for EV-charging) to a suitable power consumption level. The design of such strategies may be either centralized (in which there is a single decision-maker controlling all strategies of consumers), or decentralized (in which there are several decision-makers, each of them representing a consumer). We analyze both scenarios by exploiting the theory from formal methods, game theory and optimization. More specifically, the power consumption scheduling problem can be modeled using Markov decision processes and stochastic games. For instance, probabilities provide a way to model the environment of the electrical system, namely: the noncontrolable part of the total consumption (e.g., the non-EV consumption). The controllable consumption can be adapted to the constraints of the distribution network (e.g., to the maximum shutdown temperature of the electrical transformer), and to their objectives (e.g., all EVs are recharged). At first glance, this can be seen as a stochastic system with multi-constraints objectives. Therefore, the contributions of this thesis also concern the area of multi-criteria objective models, which allows one to pursue several objectives at the time such as having strategy designs functionally correct and robust against changes of the environment.