Add to ORKGAbstract. Tree Regular Model Checking is the name of a family of tech-niques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. We are interested in show-ing that a set of states Bad can not be reached from the set of initial states. Since the set of reachable is in general not computable, we focus on a computation of an over-approximation of the set of reachable states. A main obstacle is to be able to compute an over-approximation precise enough that does not intersect Bad i.e. a conclusive approximation. This notion of precision is often defined by a very technical parameter of tech-niques implementing this over-approximation approach. In this paper, we propose a new charact...