# A Counting Semantics for Monitoring LTL Specifications over Finite Traces

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

## Key facts

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

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

- [Pointwise-in-Time Explanation for Linear Temporal Logic Rules](https://mlsanity.com/paper/2306.13956/) (2023)

## Abstract (arXiv)

We consider the problem of monitoring a Linear Time Logic (LTL) specification that is defined on infinite paths, over finite traces. For example, we may need to draw a verdict on whether the system satisfies or violates the property "p holds infinitely often." The problem is that there is always a continuation of a finite trace that satisfies the property and a different continuation that violates it. We propose a two-step approach to address this problem. First, we introduce a counting semantics that computes the number of steps to witness the satisfaction or violation of a formula for each position in the trace. Second, we use this information to make a prediction on inconclusive suffixes. In particular, we consider a good suffix to be one that is shorter than the longest witness for a satisfaction, and a bad suffix to be shorter than or equal to the longest witness for a violation. Based on this assumption, we provide a verdict assessing whether a continuation of the execution on the same system will presumably satisfy or violate the property.