General Monitorability of Totally Ordered Verdict Domains

Abstract

Online runtime verification is a formal dynamic technique that studies how to monitor formal specifications incrementally against an input trace. Often, an observed prefix of a behavior is not enough to emit a definite verdict and the monitor must wait to receive more information from the execution of the observed system. Monitorability classifies the set of properties depending on the feasibility to obtain a verdict after a finite observation. Havelund and Peled (Proceedings of 18th international conference on runtime verification (RV 18), Berlin, 2018) classified LTL properties according to whether an observation can be extended to a definite answer. In this paper we present a framework that extends the classification of Havelund and Peled to verdict domains that are richer than Booleans, obtaining a monitorability setting under which some of the verdicts (but not others) can be discarded after a sequence of observations. We study the instance of this setting to quantitative temporal logics and we illustrate using examples the different elements of the taxonomy. Finally, we also consider how assumptions on the set of behaviors can affect monitorability.