La thèse se situe à la charnière de l'informatique théorique et de la logique mathématique. Elle se concentre en particulier sur les aspects mathématiques de la vérification et du contrôle. La thèse se focalise sur l'étude de deux sous-classes d'automates hybrides: les automates temporisés pondérés et les automates hybrides o-minimaux. Concernant les automates temporisés pondérés, en introduisant un nouvel algorithme, nous donnons une caractérisation exacte de la complexité du problème d'atteignabilité optimal en prouvant qu'il est PSpace-complet. Nous prouvons que le model-checking de la logique WCTL est en général indécidable. Nous nous intéressons alors à une restriction de la logique WCTL. Nous montrons que la décidabilité du model-checking de WCTL restreint dépend de la dimension de l'automate et du fait que le temps soit discret ou dense. Finalement pour, nous prouvons que le problème de contrôle optimal est en général indécidable. Nous prouvons cependant que ce même problème est décidable pour les automates temporisés pondérés de dimension 1. En ce qui concerne les automates hybrides o-minimaux, à l'aide d'un encodage symbolique des trajectoires par des mots, nous sommes parvenus à prouver l'existence d'une bisimulation finie pour ces automates. De plus (toujours en utilisant nos encodages des trajectoires par des mots), nous avons obtenu des résultats de décidabilité pour des problèmes de jeux sur ces mêmes automates hybrides o-minimaux. Pour une classe d'automates hybrides o-minimaux, nous avons prouvé (i) que l'existence de stratégie gagnante pouvait être décidée et (ii) que ces stratégies gagnantes pouvaient être synthétisées.

In 1994, Alur and Dill introduced timed automata as a simple mathematical model for modelling the behaviour of real-time systems. In this thesis, we extend timed automata with weights. More detailed, we equip both the states and transitions of a timed automaton with weights taken from an appropriate mathematical structure. The weight of a transition determines the weight for taking this transition, and the weight of a state determines the weight for letting time elapse in this state. Since the weight for staying in a state depends on time, this model, called weighted timed automata, has many interesting applications, for instance, in operations research and scheduling. We give characterizations for the behaviours of weighted timed automata in terms of rational expressions and logical formulas. These formalisms are useful for the specification of real-time systems with continuous resource consumption. We further investigate the relation between the behaviours of weighted timed automata and timed automata. Finally, we present important decidability results for weighted timed automata.

In 1994, Alur and Dill introduced timed automata as a simple mathematical model for modelling the behaviour of real-time systems. In this thesis, we extend timed automata with weights. More detailed, we equip both the states and transitions of a timed automaton with weights taken from an appropriate mathematical structure. The weight of a transition determines the weight for taking this transition, and the weight of a state determines the weight for letting time elapse in this state. Since the weight for staying in a state depends on time, this model, called weighted timed automata, has many interesting applications, for instance, in operations research and scheduling. We give characterizations for the behaviours of weighted timed automata in terms of rational expressions and logical formulas. These formalisms are useful for the specification of real-time systems with continuous resource consumption. We further investigate the relation between the behaviours of weighted timed automata and timed automata. Finally, we present important decidability results for weighted timed automata.