Fast Equational Abstraction Refinement for Regular Tree Model Checking

Tree Regular model checking is the name of a family of techniques for analyzing infinite- state systems in which states are represented by trees and sets of states by tree automata. From the verification point of view, the central problem is to compute the set of reachable states providing a given transition relation. A main obstacle is that this set is in general not computable in a finite time. In this paper, we propose a new CounterExample Guided Abstraction Refinement technique that can be used to check whether a set of state can be reached from the initial set. Contrary to existing techniques, our approach relies on equational abstraction to ease the definition of approximations and on a specific model of tree automata to avoid heavy backward refinement steps.