A Counting Semantics for Monitoring LTL Specifications over Finite Traces

TL;DR

This paper introduces a counting semantics approach for monitoring LTL specifications over finite traces, enabling predictions about property satisfaction or violation despite the inherent ambiguity of finite prefixes.

Contribution

It proposes a novel counting semantics method that predicts property satisfaction or violation on finite traces by analyzing witness lengths, improving runtime monitoring accuracy.

Findings

Effective prediction of property satisfaction or violation on finite traces

Provides a method to handle inconclusive suffixes in runtime monitoring

Enhances the interpretability of monitoring verdicts

Abstract

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.