标题： 决定有限树和无限字的正则语言的稀疏性 显示英文标题

标题： Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words

摘要： 我们研究了有限树和无限字上的正则语言的稀疏性概念。一棵树的语言被称为稀疏的，如果该语言中$n$节点树的相对数量趋于零，而无限字的语言被称为稀疏的，如果它在伯努利概率空间中测度为零。我们证明了正则树语言和正则无限字语言的稀疏性是可判定的。对于树，我们通过禁止子树和树自动机给出了特征描述，从而得出一个线性时间的判定过程。对于无限字，我们通过前缀完整性给出了特征描述，并提供了一个新的可判定性的证明。此外，在非稀疏的情况下，我们的算法计算出一个可测的接受字子集，可以在几乎必然模型检测中作为反例。我们的研究结果在基于自动机的模型检测、形式验证和XML模式等方面有应用。 显示英文摘要

摘要： We study the notion of sparseness for regular languages over finite trees and infinite words. A language of trees is called sparse if the relative number of $n$-node trees in the language tends to zero, and a language of infinite words is called sparse if it has measure zero in the Bernoulli probability space. We show that sparseness is decidable for regular tree languages and for regular languages of infinite words. For trees, we provide characterisations in terms of forbidden subtrees and tree automata, leading to a linear time decision procedure. For infinite words, we present a characterisation via infix completeness and give a novel proof of decidability. Moreover, in the non-sparse case, our algorithm computes a measurable subset of accepted words that can serve as counterexamples in almost-sure model checking. Our findings have applications to automata based model checking in formal verifications and XML schemas, among others.