Regular tree model checking

Abstract

In this paper, we present an approach for algorithmic verification of infinite-state systems with a parameterized tree topology. Our work is a generalization of regular model checking, where we extend the work done with strings toward trees. States are represented by trees over a finite alphabet, and transition relations by regular, structure preserving relations on trees. We use an automata theoretic method to compute the transitive closure of such a transition relation. Although the method is incomplete, we present sufficient conditions to ensure termination. We have implemented a prototype for our algorithm and show the result of its application on a number of examples. © Springer-Verlag Berlin Heidelberg 2002.