若初次未成：通过多次执行实现可监控性的扩展
计算机科学中的逻辑
2025-05-21 v3
摘要
本文研究分支时间性质在多大程度上可通过运行时监控器得到充分验证。我们脱离监控仅限于单次系统执行的经典设定，考察在多次运行上监控系统时所增强的观察能力。为确保结果的通用性，我们聚焦于以模态 μ-演算表达的分支时间性质，这是一种被充分研究的基础逻辑，并被最先进的模型检测器所使用。我们的结果表明，所提设定可系统性地扩展先前已确立的分支时间性质的可监控性界限。随后我们通过将其实例化以验证基于 actor 的系统来验证结果。我们还证明了刻画性质句法结构与所需系统运行次数之间对应关系的界限。
引用
@article{arxiv.2306.05229,
title = {If At First You Don't Succeed: Extended Monitorability through Multiple Executions},
author = {Antonis Achilleos and Adrian Francalanza and Jasmine Xuereb},
journal= {arXiv preprint arXiv:2306.05229},
year = {2025}
}