On probabilistic monitorability

Abstract

This paper investigates monitorability in the context of probabilistic systems. We specify how monitor verdicts, reached over finite (partial) traces, can be given a probabilistic interpretation. For monitors that are used to verify properties at runtime, we also relate their probabilistic verdicts to the probability that a trace satisfies the property of interest. This leads us to define probabilistic monitor soundness and completeness, which are then used to formulate probabilistic monitorability. Surprisingly, we show that the resulting notions coincide with standard monitorability definitions from the literature. This allows us to transfer prior results from the standard setting to the probabilistic realm.