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 there exist a positive integer n and terms t0,t1,...,tn such that t0set membership, variantL, tn=t and for every 0less-than-or-equals, slanti