Synthèse Quantitative – QuaSy

Les systèmes réactifs sont des systèmes qui interagissent de façon continue avec un environnement qu'ils ne contrôlent pas. Le but de la synthèse réactive est de construire des systèmes corrects directement à partir de leurs spécifications. Les spécifications quantitatives sont capables de décrire non seulement les comportements admissibles, mais aussi leur désirabilité, dû à leur coût, leur consommation d'énergie ou leur utilité, par exemple. L'objectif de la synthèse quantitative est de construire des systèmes qui optimisent leur comportement par rapport à une telle spécification.

La faisabilité de la synthèse dépend en grande partie de la spécification. En particulier, le non-déterminisme dans le formalisme de spécification tend à conduire à l'intractabilité ou même à l'indécidabilité. Malheureusement, les formalismes déterministes sont plus restrictifs. Les automates déterministes en histoire sont un formalisme intermédiaire qui permet un non-déterminisme réduit. Il est particulièrement adapté aux problèmes de synthèse : en effet, la synthèse de spécifications déterministes en histoire n'est pas plus difficile que celle de spécifications déterministes, et pourtant le déterminisme en histoire peut être plus succinct ou même plus expressif que le déterminisme, selon le type d'automate étudié.

Le but de ce projet est d'exploiter le déterminisme en histoire pour la synthèse réactive quantitative.

Le premier objectif est d'établir les relations entre les différentes généralisations du déterminisme en histoire au cadre quantitatif. Le second objectif est d'établir les propriétés des automates quantitatifs déterministes en histoire en tant que formalisme de spécification. L'objectif final du projet est de développer de nouveaux algorithmes pour la synthèse quantitative, en utilisant l'observation récente que ce problème est intimement lié au problème de décider si un automate est déterministe en histoire.