A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2008

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.
Fichier principal
Vignette du fichier
RR-6411.pdf (187.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00204579 , version 1 (15-01-2008)
inria-00204579 , version 2 (15-01-2008)

Identifiers

  • HAL Id : inria-00204579 , version 2

Cite

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⟩
157 View
313 Download

Share

Gmail Facebook X LinkedIn More