If At First You Don’t Succeed: Extended Monitorability through Multiple Executions

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.