# A Metric for Linear Temporal Logic

arXiv: https://arxiv.org/abs/1812.03923 · HTML: https://mlsanity.com/paper/1812.03923/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Nov 2018.

## Built on by (most cited first, 1 of 1)

- [Regular Decision Processes for Grid Worlds](https://mlsanity.com/paper/2111.03647/) (2021)

## Abstract (arXiv)

We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.