Monitorability of Expressive Verdicts

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. Monitorability classifies the set of properties depending on the feasibility to obtain a verdict after a finite observation. Havelund and Peled 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 two instances of this setting, quantitative temporal logics and partially ordered domains for stream runtime verification, and we illustrate using examples the different elements of the taxonomy. Finally, we also consider how assumptions on the set of behaviors can improve monitorability, and how imprecise observations can impair monitorability.