A theoretical limit for safety verification techniques with regular fix-point computations

摘要

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 there exist a positive integer n and terms t_0,t_1,...,t_n such that t_0 ∈ L, t_n=t and for every 0 ≤ i < n, (t_i, t_(i+1)) ∈ R. 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.