Apprentissage des propriétés de temps ramifié en CTL et ATL via la résolution de contraintes

Nous abordons le problème d'apprentissage des propriétés temporelles à partir du comportement à temps ramifié des systèmes. Les recherches existantes dans ce domaine se sont principalement concentrées sur l'apprentissage des propriétés temporelles linéaires spécifiées à l'aide de logiques populaires, telles que la logique temporelle linéaire (LTL) et la logique temporelle de signal (STL). Les logiques à temps ramifié telles que la logique d'arbre de calcul (CTL) et la logique temporelle alternée (ATL), bien qu'elles soient largement utilisées pour spécifier et vérifier des systèmes distribués et multi-agents, n'ont pas reçu une attention adéquate. Ainsi, dans cet article, nous étudions le problème de l'apprentissage des formules CTL et ATL à partir d'exemples de comportement système. Comme entrée pour les problèmes d'apprentissage, nous nous basons sur les représentations typiques du comportement ramifié sous forme de structures de Kripke et de structures de jeux concurrents, respectivement. Étant donné un échantillon de structures, nous apprenons des formules concises en encodant le problème d'apprentissage en un problème de satisfaisabilité, notamment en encodant symboliquement à la fois la recherche de formules potentielles et leurs algorithmes de vérification de modèle basés sur des points fixes. Nous étudions également le problème de décision de vérification de l'existence de formules ATL potentielles pour un échantillon donné. Nous avons implémenté nos algorithmes dans un prototype Python et les avons évalués pour extraire plusieurs formules CTL et ATL courantes utilisées dans des applications pratiques.