一句话：研究利用多次系统运行监控分支时间性质，证明可系统扩展传统可监控性边界并给出运行次数界。
本文关注运行时监控能否充分验证分支时间性质。传统监控通常局限于系统的单次执行，作者因此转向多次运行的监控场景，考察其增强的观察能力。为保证一般性，论文以模态 μ 演算作为分支时间性质的形式基础，系统研究多次执行下的可监控性。结果表明，该设置能够系统性地扩展既有分支时间性质的可监控性边界；作者还证明了一类界，刻画性质语法结构与所需系统运行次数之间的对应关系。最后，作者将结果实例化到基于 actor 的系统验证中，以说明方法的适用性。
This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited to a single system execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality, we focus on branching-time properties expressed in the modal µ-calculus, a well-studied foundational logic. Our results show that the proposed setup can systematically extend established monitorability limits for branching-time properties. We validate our results by instantiating them to verify actor-based systems. We also prove bounds that capture the correspondence between the syntactic structure of a property and the number of required system runs.
DOI 原文 ·
@inproceedings{paperbot8681,
title = {If At First You Don’t Succeed: Extended Monitorability through Multiple Executions},
author = {Antonis Achilleos and Adrian Francalanza and Jasmine Xuereb},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00054}
}