  Finding models for linear-time properties is a central problem in
verification and planning. We study the distribution of linear-time models by
investigating the density of linear-time properties over the space of
ultimately periodic words. The density of a property over a bound n is the
ratio of the number of lasso-shaped words of length n that satisfy the property
to the total number of lasso-shaped words of length n. We investigate the
problem of computing the density for both linear-time properties in general and
for the important special case of omega-regular properties. For general
linear-time properties, the density is not necessarily convergent and can
oscillate indefinitely for certain properties. However, we show the oscillation
can be bounded by the growth of the sets of bad- and good-prefix of the
property. For omega-regular properties, we show that the density is always
convergent and provide a general algorithm for computing the density of
omega-regular properties as well as more specialized algorithms for certain
sub-classes and their combinations.
