A Linear Temporal Logic of Frequencies on Series of Events

TL;DR

This paper presents LTLF, a new temporal logic with measure-sensitive operators for expressing and analyzing frequency properties of event sequences, bridging formal logic and empirical data.

Contribution

Introduction of LTLF, a novel temporal logic with measure-sensitive operators and modal quantifiers for formalizing and analyzing event frequencies.

Findings

LTLF enables explicit formalization of event series properties.

LTLF allows comparison between observed frequencies and ideal distributions.

The framework supports monitoring and controlling quantitative systems.

Abstract

This paper introduces LTLF, a temporal logic designed to express the frequency properties of event series in a natural but rigorous manner. By introducing novel, measure-sensitive operators, LTLF allows for the evaluation of frequencies and the prediction of future occurrences, thus providing a formal framework to monitor and control quantitative systems, such as machine learning classifiers. The core novelty lies in the introduction of original modal quantifiers associated with a standard Kripke-style semantics. These quantifiers enable the explicit formalization of event series properties and the investigation of the relationship between actual observed frequencies and ideal distributions within a single logical structure. This framework bridges the gap between formal logical reasoning and empirical observation.