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

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.