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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

An Algebraic Approach to the Equivalence Checking of Deterministic Top-down Tree Transducers

  • Deng Zhibo,
  • Tang Tianxiang,
  • Vladimir A. Zakharov

摘要

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.