Relaxing safety for metric first-order temporal logic via dynamic free variables

TL;DR

This paper introduces a new fragment of metric first-order temporal logic that ensures finite table representations, extends it with dual operators, and integrates it into a runtime verification tool, enhancing monitorability.

Contribution

The paper defines a larger fragment of metric first-order temporal logic with added operators and proves its properties, improving runtime verification capabilities.

Findings

Fragment guarantees finite table representations.

Extended fragment includes trigger and release operators.

Successfully integrated into a verification tool with formal correctness proof.

Abstract

We define a fragment of metric first-order temporal logic formulas that guarantees the finiteness of their table representations. We extend our fragment's definition to cover the temporal dual operators trigger and release and show that our fragment is strictly larger than those previously used in the literature. We integrate these additions into an existing runtime verification tool and formally verify in Isabelle/HOL that the tool correctly outputs the table of constants that satisfy the monitored formula. Finally, we provide some example specifications that are now monitorable thanks to our contributions.