Traduction d'expressions rationnelles semi-étendues en automates finis, à l'aide de formes linéaires
Jeudi 17 octobre 2024, 14:00 à 15:00
Salle de séminaire du département informatique
(LRE, EPITA)
Nous généralisons la notion de forme linéaire d'une expression rationnelle, introduite par Antimirov, pour couvrir les expressions rationnelles semi-étendues utilisées en PSL (Property SpecificationLanguage) ou SVA (SystemVerilog Assertions). Cela nécessite d'étendre la construction pour supporter de nouveaux opérateurs, et de traiter des expressions portant sur des alphabets \(\Sigma=2^{\text{AP}}\) de valuations de propositions atomiques. L'utilisation de formes linéaires pour construire des automates étiquetés par des expressions booléennes amène plusieurs heuristiques que nous évaluons. Enfin, nous étudions une variante de cette traduction vers des automates où l'acceptation porte sur les transitions : cette construction est plus naturelle et permet de produire des automates plus petits.