Monitoring Hyperproperties With Prefix Transducers

TL;DR

This paper introduces prefix transducers as a new formalism for monitoring both synchronous and asynchronous hyperproperties, enabling incremental and deterministic runtime verification.

Contribution

It presents multi-trace prefix transducers for monitoring hyperproperties, including asynchronous cases, offering a deterministic alternative to logical specifications.

Findings

Effective monitoring of asynchronous hyperproperties demonstrated

Prefix transducers outperform logical specifications in determinism

Experimental results on observational determinism monitoring

Abstract

Hyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL. When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as, for the first time, asynchronous hyperproperties. Prefix transducers map multiple input traces into one or more output traces, by incrementally matching prefixes of the input traces against expressions similar to regular expressions. The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths. The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism for runtime verification than logical specifications, which tend to be highly nondeterministic, especially in the case of asynchronous hyperproperties. We report on a set of experiments about monitoring asynchronous version of observational determinism.