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.

翻译：超性质是指关联多条执行迹的性质。此前关于超性质监控的研究主要聚焦于同步超性质，通常采用HyperLTL进行规约。在监控同步超性质时，假定所有迹以相同速度推进。本文引入（多迹）前缀转换器，并展示如何将其首次用于同步以及异步超性质的监控。前缀转换器通过将输入迹的前缀与类正则表达式进行增量匹配，将多条输入迹映射为一条或多条输出迹。在监控器的单次匹配步骤中，不同迹所消耗的前缀长度可能不等。前缀转换器具有确定性和可执行性，相较于逻辑规约（尤其在异步超性质场景下往往呈现高度非确定性），更适合作为运行时验证的中间形式化工具。我们报告了关于监控异步版本观察决定论的一组实验结果。