Approximations par réécriture pour deux problèmes indécidables
Résumé
Pour vérifier des propriétés de sûreté ou de (non-)atteignabilité par model-checking régulier, on se concentre sur une modélisation des configurations accessibles du système par des langages réguliers et des relations d'évolution par des systèmes de réécriture. Le problème d'atteignabilité est indécidable dans de nombreux formalismes, et l'approche générale consiste à étudier et/ou à combiner des cas particuliers. Nous nous intéressons à l'approche par approximation pour semi-décider ce problème de vérification. Dans ce papier, nous exploitons l'analyse d'atteignabilité pour deux problèmes indécidables pour les machines de Turing : vacuité d'un langage et appartenance d'un mot à un langage. Nous proposons une modélisation et montrons comment les approximations par réécriture permettent de semi-décider ces problèmes. Cette approche a été implantée et expérimentée.
Domaines
Théorie et langage formel [cs.FL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...