Key points are not available for this paper at this time.
La logique temporelle est un cadre pour représenter et raisonner sur des propositions qui évoluent dans le temps. Elle est couramment utilisée pour spécifier des exigences dans divers domaines, y compris les systèmes matériels et logiciels, ainsi que la robotique. L'extraction de spécifications ou la génération de formules consiste à extraire des formules de logique temporelle à partir de traces de système et a de nombreuses applications, telles que la détection de bogues et l'amélioration de l'interprétabilité. Bien qu'il y ait eu un essor des méthodes basées sur l'apprentissage profond pour la vérification de la satisfaisabilité en logique temporelle ces dernières années, la littérature sur l'extraction de spécifications a pris du retard dans l'adoption de méthodes d'apprentissage profond malgré leurs nombreux avantages, tels que l'évolutivité. Dans cet article, nous introduisons des modèles autorégressifs capables de générer des formules de logique temporelle linéaire à partir de traces, dans le but de résoudre le problème d'extraction de spécifications. Nous proposons plusieurs architectures pour cette tâche : encodeur-décodeur transformateur, transformateur uniquement décodeur et Mamba, qui est une alternative émergente aux modèles transformateurs. De plus, nous concevons une métrique pour quantifier la distinctivité des formules générées et un algorithme simple pour faire respecter les contraintes de syntaxe. Nos expériences montrent que les architectures proposées donnent des résultats prometteurs, générant des formules correctes et distinctes à une fraction du coût de calcul nécessaire pour la référence combinatoire.
Işık et al. (Fri,) ont étudié cette question.