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

Yohan Boichut (1, 2) , Pierre-Cyrille Heam (3)

1 PAREO - Formal islands: foundations and applications
2 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
3 CASSIS - Combination of approaches to the security of infinite states systems

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

Mots clés: Reachability problem; Regular tree languages; Formal methods; Theoretical limit

Domaines: Informatique et langage [cs.CL]

Yohan Boichut, Pierre-Cyrille Heam. A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations. Information Processing Letters, 2008, 108 (1), pp.1-2. ⟨10.1016/j.ipl.2008.03.012⟩. ⟨inria-00328487⟩