强双幺半群上加权树自动机的清晰确定化

我们考虑强双幺半群上的加权树自动机(wta)及其初始代数语义和跑动语义。存在这些语义不同的wta；然而，对于自底向上确定型wta和半环上的wta，该差异消失。若wta是自底向上确定型且每个转移由强双幺半群的单位元之一加权，则称其为清晰确定型。我们证明由清晰确定型wta识别的加权树语言类与可识别步映射类相同。此外，我们研究以下两个清晰确定化问题：给定wta ${\cal A}$，(a)是否存在计算${\cal A}$初始代数语义的清晰确定型wta，以及(b)是否存在计算${\cal A}$跑动语义的清晰确定型wta？我们证明${\cal A}$的Nerode代数${\cal N}({\cal A})$的有限性蕴含(a)的肯定回答，且${\cal A}$的有限阶性质蕴含(b)的肯定回答。我们给出保证${\cal N}({\cal A})$有限性的充分条件以及保证${\cal A}$有限阶性质的充分条件。同时，若${\cal N}({\cal A})$有限，我们提供根据(a)构造清晰确定型wta的算法，类似地若${\cal A}$具有有限阶性质则根据(b)提供算法。我们证明任意wta ${\cal A}$是否可清晰确定化是不可判定的。我们还证明${\cal N}({\cal A})$的有限性与${\cal A}$的有限阶性质均不可判定。