Extending the Limits of Monitorability

Abstract

One of the most fundamental and long-standing issues in computer science is making sure that a system behaves as intended. To address this challenge, systems may be verified dynamically using a lightweight monitoring technique called runtime verification. Even though runtime verification circumvents issues associated with traditional techniques, it is limited by the fact that observations are typically constrained to the current computation path of the system. This limitation is even more acute for correctness properties describing the system’s computational graph, known as branching-time properties. This thesis investigates whether runtime verification can be extended to meaningfully verify a wider range of branching-time properties. We depart from the classical setup where monitoring is limited to a single execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal mu-calculus, a well-studied foundational logic used by state-of-the-art model checkers. As part of a comprehensive theory, the first part of this thesis focuses on deterministic systems and demonstrates that the proposed multi-run monitoring setup can systematically extend previously established monitorability limits for branching-time properties. The second part extends the multi-run framework and corresponding results to systems that may exhibit non-deterministic behaviour. To show that the proposed setup is implementable, the third part outlines the steps for a full automation, as well as proves bounds that capture the correspondence between the syntactic structure of a property and the number of system runs required to adequately verify it. We also validate our results by instantiating the proposed multi-run monitoring setup to verify actor-based concurrent systems, a widely used concurrency paradigm. Given that these systems are inherently non-deterministic, the fourth part presents a general study of a highly non-deterministic calculus, where we systematically explore how the defining characteristics of the actor model enable the recovery of a certain degree of determinism.