On Safety Properties and Their Monitoring

From FSL
Jump to: navigation, search

Scientific Annals of Computer Science

On Safety Properties and Their Monitoring
Grigore Rosu
SACS, Volume 22(2), pp 327-365. 2012
Abstract. This paper addresses the problem of runtime verification from a foundational perspective, answering questions like Is there a consensus among the various definitions of a safety property? (Answer: Yes), How many safety properties exist? (Answer: As many as real numbers), How difficult is the problem of monitoring a safety property? (Answer: Arbitrarily complex), Is there any formalism that can express all safety properties? (Answer: No), etc. Various definitions of safety properties as sets of execution traces have been proposed in the literature, some over finite traces, others over infinite traces, yet others over both finite and infinite traces. By employing cardinality arguments and a novel notion of persistence, this paper first establishes the existence of bijective correspondences between the various notions of safety property. It then shows that safety properties can be characterized as always past properties. Finally, it proposes a general notion of monitor, which allows to show that safety properties correspond precisely to the monitorable properties, and then to establish that monitoring a safety property is arbitrarily hard.
PDF, MOP, DOI, SACS, BIB

Technical Report

On Safety Properties and Their Monitoring
Grigore Rosu
Technical report UIUCDCS-R-2007-2850, February 2007
Abstract. Various definitions of safety properties as sets of execution traces have been introduced in the literature, some over finite traces, others over infinite traces, yet others over both finite and infinite traces. By employing cardinality arguments, this paper first shows that these notions of safety are ultimately equivalent, by showing each of them to have the cardinal of the continuum. It is then shown that all safety properties can be characterized as "always past" properties, and then that the problem of monitoring a safety property can be arbitrarily hard. Finally, two decidable specification formalisms for safety properties are discussed, namely extended regular expressions and past time LTL. It is shown that monitoring the former requires non-elementary space. An optimal monitor synthesis algorithm is given for the latter; the generated monitors run in space linear with the number of temporal operators and in time linear with the size of the formula.
PDF, ZIP, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation