Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866918083393748992 |
|---|---|
| author | Eickmeyer, Kord Schindling, Georg |
| author_facet | Eickmeyer, Kord Schindling, Georg |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_03465 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words Eickmeyer, Kord Schindling, Georg Formal Languages and Automata Theory 68Q45 F.4.3 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. |
| title | Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words |
| topic | Formal Languages and Automata Theory 68Q45 F.4.3 |
| url | https://arxiv.org/abs/2507.03465 |