Monitorability for Runtime Verification

Runtime verification (RV) allows analyzing execution traces using formal techniques. In particular, it permits monitoring the execution of a system against a temporal specification, commonly to detect failures to satisfy it. Online RV observes a sequence of events and is required to provide a verdict whether it concludes that the execution satisfies or falsifies the specification. As at any moment, only a portion of the complete execution may have been reported, the RV algorithms strive to provide a verdict based on the observed prefix. Monitorability of a temporal property is the ability to provide positive or negative verdicts after observing a finite prefix of the execution. We classify temporal properties based on their monitorability and present related monitoring algorithms. A common practice in runtime verification is to concentrate on the class safety properties, where if a failure occurs, it can always be detected in finite time. In the second part of the paper we concentrate on monitoring safety properties and their place among the other classes of properties in terms of algorithms and complexity.