Efficiently Computable Temporal Robustness for a Practical STL Fragment
Vendredi 07 février 2025
In 2024 at QEST+FORMATS 2024, Rino, Foughali and Asarin proposed a new robustness measure for a subset of STLs based on a new distance on timed signals. We extend this work by implementing the algorithms given there and using this measure to compare different insulin controllers for diabetic patients.
Réductions efficaces de machines de Mealy
Vendredi 17 mars 2023
Nous revisitons le problème de la réduction des machines de Mealy incomplètement spécifiées avec la synthèse réactive en tête. Nous proposons deux techniques : la première est inspirée de l'outil MeMin et résout le problème de minimisation, la seconde est une nouvelle approche dérivée des réductions basées sur la simulation mais ne garantit pas forcément une machine minimale. Nous soutenons cependant qu'elle offre un assez bon compromis entre la taille de la machine résultante et les performances. Les méthodes proposées sont comparées à MeMin sur une large collection de cas de test composés d'instances bien connues ainsi que de nouvelles instances.
Transformations d’ω-automates pour la synthèse de contrôleurs réactifs
Vendredi 30 septembre 2022
La synthèse vise à produire un système correct à partir de spécifications. Une approche pour résoudre ce problème consiste à traduire la spécification en un jeu de parité dont la stratégie gagnante encode le système. Dans cet exposé nous verrons deux méthodes permettant de produire des automates de parité. La première s’appuie sur l’amélioration et la combinaison de procédures nouvelles ou existantes. La seconde est un algorithme de Casares et al. apportant une garantie d’optimalité du résultat. Dans un deuxième temps, nous verrons comment nous réduisons le système obtenu. Deux types de réductions seront abordées. La première permet d’obtenir un résultat optimal mais pas la seconde qui privilégie le temps de traitement.
Practical “Paritizing” of Emerson-Lei Automata
Lundi 18 octobre 2021
We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.
