Simulation-Based Iteration of Tree Transducers
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.
KeywordsEquivalence Relation Model Check Binary Relation Transitive Closure Reachable State
- [ABH+97]Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997)Google Scholar
- [CDG+99]Common, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (October 1999) (not yet published) Google Scholar
- [HHK95]Henzinger, M., Henzinger, T., Kopke, P.: Computing simulations on finite and infinite graphs. In: Proc.36th Annual Symp. Foundations of Computer Science, pp. 453–463 (1995)Google Scholar
- [Tho90]Thomas, W.: Automata on infinite objects. Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics, 133–192 (1990)Google Scholar