Dans le cadre de la vérification formelle de programmes, nous étudions des systèmes placés dans un environnement extérieur : il s'agit de guider ou contrôler le système pour qu'il satisfasse certaines propriétés. Pour modéliser l'écoulement du temps, nous nous intéressons aux systèmes hybrides et aux logiques temporisées. Nous étudions les systèmes hybrides o minimaux pondérés et établissons que ce modèle est expressif mais analysable puisque le model checking ainsi que le contrôle optimal sont décidables, ces problèmes étant indécidables pour les automates temporisés. Nous étudions également les logiques temporisées et montrons que la logique TPTL est strictement plus expressive que MTL, prouvant une conjecture énoncée par Alur et Henzinger au début des années 1990. Enfin nous introduisons une classe d'automates paramétrés par des opérateurs et obtenons des résultats génériques d'expressivité entre automates et logiques, qui peuvent notamment s'appliquer à MTL+Past.