Ain't No Stopping Us Monitoring Now
Abstract
Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this paper, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of Linear Temporal Logic (LTL).
Keywords
Cite
@article{arxiv.2211.11544,
title = {Ain't No Stopping Us Monitoring Now},
author = {Luca Ciccone and Francesco Dagnino and Angelo Ferrando},
journal= {arXiv preprint arXiv:2211.11544},
year = {2022}
}