Florian Renkin

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.

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.

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.