通过动态自由变量放宽度量一阶时序逻辑的安全性
计算机科学中的逻辑
2022-06-20 v1
摘要
我们定义了度量一阶时序逻辑公式的一个片段，保证其表表示（table representation）的有限性。我们将该片段的定义扩展到涵盖时序对偶算子 trigger 和 release，并表明我们的片段严格大于文献中先前使用的那些。我们将这些补充集成到一个现有的运行时验证工具中，并在 Isabelle/HOL 中形式化验证该工具正确输出满足被监控公式的常量表。最后，我们提供了一些得益于我们的贡献而现在可监控的示例规约。
引用
@article{arxiv.2206.08714,
title = {Relaxing safety for metric first-order temporal logic via dynamic free variables},
author = {Jonathan Julian Huerta y Munive},
journal= {arXiv preprint arXiv:2206.08714},
year = {2022}
}
备注
12 pages, conference, appendix