Deciding Sparseness of Regular Languages of Finite Trees and Infinite Words

TL;DR

This paper investigates the decidability of sparseness in regular languages over finite trees and infinite words, providing characterisations and decision procedures with applications in formal verification and XML schemas.

Contribution

It introduces new characterisations and linear-time decision procedures for sparseness in regular tree and infinite word languages, with practical applications.

Findings

Decidability of sparseness for regular tree languages

Decidability of sparseness for regular languages of infinite words

Algorithm for computing counterexamples in non-sparse cases

Abstract

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.