An Algebraic Approach to the Equivalence Checking of Deterministic Top-down Tree Transducers
摘要
For many classes of automata, denotational semantics provides suitable means for specifying functions or relations \(\llbracket s \rrbracket _\pi \) , computed in all states s of an automaton \(\pi \) , through the system of algebraic equations. By adding to this system an equation \(\llbracket s_1 \rrbracket _\pi =\llbracket s_2 \rrbracket _\pi \) which declares that \(\pi \) computes in some states \(s_1\) and \(s_2\) the same function or relation we reduce the equivalence checking problem to that of checking the solvability of the system of equations obtained thus. In general, this problem is intractable, but when dealing only with deterministic automata the solvability checking can be performed efficiently by means of a technique very much similar to Gaussian variable elimination used in linear algebra. In this paper we show that equivalence of total deterministic tree transducers can be resolved just as efficiently using this fairly general method. Moreover, this method can be very easy adapted for computing the most general unifiers of parameterized deterministic tree transducers.