The Density of Linear-time Properties

TL;DR

This paper investigates the distribution of linear-time properties by analyzing the density of models over ultimately periodic words, providing algorithms for omega-regular properties and insights into oscillations in general properties.

Contribution

It introduces methods to compute the density of linear-time properties, especially omega-regular ones, and analyzes oscillation behavior in general properties.

Findings

Density for omega-regular properties always converges.

Algorithms for computing density of omega-regular properties are provided.

Oscillation in density can be bounded by prefix set growth.

Abstract

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.