A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations

Abstract : In computer aided verification, the reachability problem is particularly relevant for safety analyses. Given a regular tree language L, a term t and a relation R, the reachability problem consists in deciding whether a sequence of terms, beginning with a term of L and terminating on t and such that two successive terms of this sequence are in relation according to R, is constructable. In this case, the term t is said to be reachable, otherwise it is said unreachable. This problem is decidable for particular kinds of relations, but it is known to be undecidable in general, even if L is finite. Several approaches to tackle the unreachability problem are based on the computation of an R-closed regular language containing L. In this paper we show a theoretical limit to this kind of approaches for this problem.
Type de document :
Rapport
[Research Report] RR-6411, INRIA. 2008, pp.6
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00204579
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 15 janvier 2008 - 12:57:13
Dernière modification le : jeudi 15 février 2018 - 08:48:03
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:58:03

Fichiers

RR-6411.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00204579, version 2

Citation

Yohan Boichut, Pierre-Cyrille Heam. A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations. [Research Report] RR-6411, INRIA. 2008, pp.6. 〈inria-00204579v2〉

Partager

Métriques

Consultations de la notice

234

Téléchargements de fichiers

105