arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2507.03465cs.FL
收藏

判定有限树与无限词上正则语言的稀疏性

Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words

Kord Eickmeyer, Georg Schindling

AI总结:

本文研究有限树与无限词上正则语言的稀疏性,证明其可判定性,并分别给出基于禁止子树/树自动机和中缀完备性的刻画,同时为非稀疏情形提供可用于几乎必然模型检验的反例构造方法。

摘要:

我们研究有限树和无限词上正则语言的稀疏性概念。若一个树语言中 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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑