The Density of Linear-Time Properties

DOI10.1007/978-3-319-68167-2_10MaRDI QIDQ5096080zbMATH OpenOpenAlexFDO

Publication date 12 August 2022

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1803.08890

Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

Cited in

(5)

This page was built for publication: The Density of Linear-Time Properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096080)