8481 articles  [english version]

inria-00204579, version 2

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

Yohan Boichut 1, Pierre-Cyrille Heam 2

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 :  PAREO (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • 2 :  Laboratoire d'Informatique de Franche-Comté (LIFC)
  • 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
  • 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