inria-00204579, version 2
A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations
N° RR-6411 (2008)
Résumé : 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.
- 1 :
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- 2 :
- Université de Franche-Comté : EA4269
- Domaine : Informatique/Autre
- Mots-clés : reachability problem – regular tree languages – undecidable – theoretical limit
- Référence interne : RR-6411
- Versions disponibles : v1 (15-01-2008) v2 (15-01-2008)
- inria-00204579, version 2
- http://hal.inria.fr/inria-00204579
- oai:hal.inria.fr:inria-00204579
- Contributeur :
- Soumis le : Mardi 15 Janvier 2008, 12:57:13
- Dernière modification le : Lundi 3 Mars 2008, 14:08:56




Documents associés

Exporter