This paper investigates the observational capabilities of monitors that can observe a system over multiple runs. We study how the augmented monitoring setup affect the class of properties that can be verified at runtime, focussing on branching-time properties expressed in the modal mu-calculus. Our results show that the setup can be used to systematically extend previously established monitorability limits. We also prove bounds that capture the correspondence between the syntactic structure of a branching-time property and the number of system runs required to conduct the verification.

翻译：本文研究了能够对系统进行多次运行观测的监测器的观测能力。我们探讨了增强监测设置如何影响可在运行时验证的属性类别，重点聚焦于以模态μ-演算表达的分支时间属性。研究结果表明，该设置可用于系统性地扩展先前确立的可监测性界限。我们还证明了界定分支时间属性语法结构与验证所需系统运行次数之间对应关系的边界。