Robust Monitoring of Linear Temporal Properties
share
Runtime verification is commonly used to detect and, if possible, react to the violation of desired properties in safety critical systems. Also common is the use of temporal logics to specify the desired properties. However, if properties are expressed in two-valued logics, such as Linear-time Temporal Logic (LTL), monitoring them often yields insufficient results: when the property is satisfied, there is nothing we need to do; once it is violated, there may be nothing we can do. To overcome this problem, logics such as robust LTL (rLTL) allow for detecting the degree of a violation: in this way, violations may be mitigated. In this paper we solve the rLTL monitoring problem by constructing a deterministic monitoring automaton for each possible degree of violation of the specification. The automaton indicates whether: 1) the property is already satisfied with respect to that degree and thus needs no further attention, 2) is still undetermined, or 3) is already violated. Violation of a property by a small degree can then be used to trigger appropriate safety measures preventing the violation of the same property to a higher degree. As the size of the monitoring automata is doubly-exponential in the size of the rLTL formula, robustly monitoring systems comes without penalty in terms of space or time when compared to classical LTL monitoring.
READ FULL TEXT