A Metric for Linear Temporal Logic
Logic in Computer Science
2018-12-11 v1 Formal Languages and Automata Theory
Abstract
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.
Keywords
Cite
@article{arxiv.1812.03923,
title = {A Metric for Linear Temporal Logic},
author = {Íñigo Íncer Romeo and Marten Lohstroh and Antonio Iannopollo and Edward A. Lee and Alberto Sangiovanni-Vincentelli},
journal= {arXiv preprint arXiv:1812.03923},
year = {2018}
}