噪声运行时验证的形式化框架

中文摘要 AI 辅助

我们引入了逻辑EDMon——一种旨在对噪声运行时验证中的可监控性概念进行建模的认识动态逻辑。我们定义并解释了其语法和语义，并探讨了EDMon与可监控性及噪声运行时验证概念之间的联系。随后，我们证明了EDMon足以捕捉噪声运行时验证文献中的许多结果，并编目了它与邻近逻辑的关系，描述了其一大类定理。

英文摘要

We introduce the logic EDMon---an epistemic dynamic logic meant to model monitorability concepts in noisy runtime verification. Its syntax and semantics are defined and explained and the connection between EDMon and monitorability and noisy runtime verification concepts is explored. We then demonstrate that EDMon is sufficient to capture many of the results in the noisy runtime verification literature and catalog its relation to nearby logics and describe a large class of its theorems.

发表机构

• Rensselaer Polytechnic Institute（伦斯勒理工学院）
• Kansas State University（堪萨斯州立大学）
• Tohoku University（东北大学）

机构由 AI 辅助整理，请以论文原文为准。