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.

翻译：我们定义了一组一阶标准时间逻辑公式的碎片,以保证其表态的有限性。我们扩展了我们的碎片定义,以涵盖时间上的双重操作器触发和释放,并表明我们的碎片比文献中以前使用的要大得多。我们将这些增加的碎片纳入现有的运行时间核查工具,并在伊莎贝尔/霍尔正式核实该工具正确输出了符合监测公式的常数表。最后,我们提供了一些由于我们的贡献而现在可以监测的示例。