论文标题
通过动态自由变量的度量一阶时间逻辑的放松安全性
Relaxing safety for metric first-order temporal logic via dynamic free variables
论文作者
论文摘要
我们定义了公制的一阶时间逻辑公式的片段，该公式可以保证其表表示的有限性。我们扩展了片段的定义，以涵盖时间双重操作员触发并释放，并表明我们的片段严格比以前在文献中使用的片段大。我们将这些添加物集成到现有的运行时验证工具中，并在Isabelle/HOL中正式验证该工具正确输出满足受监视公式的常数表。最后，我们提供了一些示例规格，这些规范现在可以根据我们的贡献来监视。
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.
