Simulation-Based Iteration of Tree Transducers

Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, Ahmed Rezine

Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. The central problem is to compute the transitive closure of a transducer. A main obstacle is that the set of reachable states is in general not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure.We have implemented and applied our technique to several protocols.

In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2005,

Last version (pdf) 2005