Runtime Monitoring of Nonterminating Systems for Alternation-Free HyperLTL Formulas

Abstract Runtime monitoring for a hyperproperty is aimed at discovering the relationships among the execution traces of the system under monitoring at run time so that a verdict of satisfaction or violation can be given on the system. For nonterminating systems, whose traces are of infinite length, such relationships can hardly be established as the monitor can naturally observe the prefixes of only one single running trace of the system. In order to deal with this problem, we suggest that the monitor be provided with an over-approximation of the set of possible traces of the nonterminating system, and at the same time, be able to observe the growing prefixes of a fixed number of traces produced by the same number of running copies of the system. To devise such monitors, we first introduce the concept of k-trace monitorability of a hyperproperty given an over-approximation of the system under monitoring, which essentially says it is always hoped that a verdict will be issued on the system if k growing prefixes of the traces in the given over-approximation can be observed at run time. We also propose an algorithm that takes an alternation-free HyperLTL formula together with a Kripke structure representing the given over-approximation and decides if the formula is k-trace monitorable for a given positive integer k. The idea underlying this algorithm is then used to suggest a generic runtime monitor for k-trace monitorable alternation-free HyperLTL formulas, which is a Moore machine running on the prefixes of the traces produced by k exact copies of the nonterminating system under monitoring.