度量时序逻辑中高效可监控公式的综合
人工智能
2023-10-27 v1 计算机科学中的逻辑
摘要
在运行时验证中，为监控系统执行而手动形式化规约是一个繁琐且易出错的过程。为解决此问题，我们考虑从系统执行中自动综合形式化规约的问题。为展示我们的方法，我们考虑流行的规约语言度量时序逻辑（MTL），它特别适用于为信息物理系统（CPS）指定时序性质。大多数综合时序逻辑公式的经典方法旨在最小化公式规模。然而，对于监控效率而言，除规模外，规约所需的“前瞻量”也变得相关，尤其是对于安全关键应用。我们形式化了这一概念，并设计了一种学习算法，可综合具有有界前瞻的简洁公式。为此，我们的算法将综合任务归约为线性实算术（LRA）中的一系列可满足性问题，并从满足性赋值中生成 MTL 公式。该归约使用一种基于 LRA 对流行 MTL 监控过程的新型编码。最后，我们在名为 TEAL 的工具中实现了我们的算法，并展示了其在 CPS 应用中综合高效可监控 MTL 公式的能力。
引用
@article{arxiv.2310.17410,
title = {Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic},
author = {Ritam Raha and Rajarshi Roy and Nathanael Fijalkow and Daniel Neider and Guillermo A. Perez},
journal= {arXiv preprint arXiv:2310.17410},
year = {2023}
}