In this talk, I will explore how observing systems across multiple executions significantly enhances the power of runtime monitors. We focus specifically on branching-time properties expressed in the modal mu-calculus—a class of properties traditionally considered the exclusive domain of static techniques like model checking. I will demonstrate how this augmented monitoring setup allows us to systematically transcend established monitorability limits. Furthermore, I will discuss the intrinsic link between the syntactic structure of a branching-time property and the specific number of system runs required to achieve definitive verification of that property.

This is joint work with Antonis Achilleos and Jasmine Xuereb.