A synthesis tool for optimal monitors in a branching-time setting

Abstract

Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branchingtime properties expressed in a variant of the modal μ-calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.