Weighted timed games : decidability, randomness and robustness

Jeux temporisé à coût : décidabilité, randomisation et robustesse Les systèmes logiciels sont omniprésents et leur fiabilité est souvent cruciale, surtout lorsqu'une défaillance peut entraîner une catastrophe humaine, environnementale ou même économique. Développées depuis de nombreuses années, les méthodes formelles, comme l'approche classique du "model-checking", sont utilisées pour prouver la correction des systèmes. Plus récemment, au lieu de les construire manuellement un nouveau paradigme émerge pour automatiquement synthétiser des systèmes corrects. Pour cela, nous nous appuyons sur la théorie des jeux qui fournit des outils mathématiques afin de modéliser le comportement de deux agents antagonistes. Dans ce contexte, deux joueurs, un contrôleur et un environnement, jouent sur le graphe des configurations du système dans lequel la condition gagnante pour le contrôleur induit la correction du système. De plus, via l'ajout de poids, ces jeux peuvent être étendus pour étudier les performances du système, comme sa consommation d'énergie. Dans ce travail, nous nous concentrons sur la synthèse de systèmes temps-réel efficaces avec une condition de victoire simple: atteindre une configuration correcte.Les jeux temporisés à coût sont des jeux à deux joueurs et à somme nulle joués dans un automate temporisé pondéré. Nous considérons l'objectif d'accessibilité optimale, dans lequel l'un des joueurs, que nous appellerons Min, veut atteindre une cible tout en minimisant le poids cumulé. Même si savoir quand Min a une stratégie (déterministe) pour garantir que la valeur obtenue est inférieure à un seuil donné, est indécidable (avec deux horloges ou plus), plusieurs conditions ont été données pour retrouver la décidabilité. L'une d'entre elles est la divergence, une autre consiste à se limiter aux jeux temporisés à coût avec une seule horloge et contenant uniquement des poids positifs. Nous étendons d'abord cette liste en considérant les jeux temporisés à coût à une horloge avec des poids arbitraires, en montrant que leur fonction de valeur peut être calculée en temps exponentiel (si les poids sont codés en unaire).Ensuite, dans de tels jeux temporisés à coût (comme dans les jeux pondérés non temporisés en présence de poids négatifs), Min peut avoir besoin d'une mémoire finie pour jouer (presque) optimalement. Il est donc tentant d'essayer d'émuler cette mémoire finie avec d'autres fonctionnalités comme en permettant aux joueurs d'utiliser des décisions stochastiques, à la fois dans le choix des transitions et des délais. Nous donnons, pour la première fois, une définition de la valeur espérée dans les jeux temporisés à coût, surmontant plusieurs défis théoriques. Nous montrons ensuite que, dans les jeux temporisés à coût divergents, la valeur stochastique est bien égale à la valeur classique (déterministe), prouvant ainsi que Min peut garantir la même valeur en n'utilisant que des choix stochastiques et sans mémoire.Enfin, les stratégies stochastiques quasi-optimales que nous synthétisons ne sont pas implémentables car elles utilisent la précision infinie des horloges dans le choix des délais ainsi qu'une connaissance précise des configurations. La robustesse est un processus connu pour encoder l'imprécision des délais dans les stratégies : elle permet au joueur Max (l'adversaire de Min) de modifier légèrement le délai choisi par Min. Dans la littérature, deux sémantiques robustes existent : la sémantique conservatrice qui vérifie la garde après la perturbation, et la sémantique excessive qui la vérifie avant. Comme pour les stratégies déterministes, déterminer si Min a une stratégie (robuste) pour garantir que la valeur est inférieure à un seuil donné, est connu pour être indécidable. En adaptant le processus d'itération de la valeur introduit par Alur et al, nous calculons la valeur (robuste) dans des jeux temporisés à coût acycliques (ou divergents avec uniquement des poids positifs) sous une sémantique conservatrice ou excessive.