Monitorable hyperproperties of nonterminating systems

Runtime monitoring for a hyperproperty is aimed at giving a verdict of satisfaction or violation on the whole system under monitoring, and not on its individual execution traces. Indeed, a monitor for a hyperproperty should naturally be able to observe prefixes of several different traces of the system and establish the relationships among them at run time. The traces of nonterminating systems, however, are of infinite length, and the monitor cannot normally observe anything other than the prefixes of only one single running trace. In this paper, we study the feasibility of monitoring nonterminating systems against hyperproperties. To do so, we introduce single-trace monitorability as a novel conception of a monitorable hyperproperty, and illustrate that the members of only one particular, small class of hyperproperties are monitorable if no prior knowledge about the system under monitoring is available. The concept of single-trace monitorability is then generalized to the environments where the monitor has access to an under/over-approximation of the set of the traces that may occur at run time. We investigate the closure properties of the set of monitorable hyperproperties given an approximation, and study the relationships among the proposed notions of monitorability.