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.

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

Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words

  • Kord Eickmeyer,
  • Georg Schindling

摘要

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.