Approximations par réécriture pour deux problèmes indécidables

Roméo Courbis (1, 2) , Pierre-Cyrille Heam (1, 2) , Pierre Jourdan (2) , Olga Kouchnarenko (1, 2)

1 CASSIS - Combination of approaches to the security of infinite states systems
2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)

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]

Roméo Courbis, Pierre-Cyrille Heam, Pierre Jourdan, Olga Kouchnarenko. Approximations par réécriture pour deux problèmes indécidables. AFADL, Jun 2010, Poitiers, France. pp.7. ⟨hal-00530341⟩