Hyperproperties specify system requirements that relate multiple executions. Reasoning about such properties naturally involves executions that play different roles: some correspond to concrete behaviors of the system under verification, while others represent idealized or alternative executions defined by the specification. We propose a framework that makes this semantic distinction explicit by distinguishing between observed and constructed traces. Constructed traces are built using generators: functions provided at specification time and invoked by monitors at runtime. Our main motivation lies in the runtime verification of hyperproperties, where only a finite view on possible executions is available. Our approach enables sound runtime verification for a broader class of hyperproperties than approaches that do not account for constructed traces, including properties with quantifier alternation, such as opacity in security, and properties defined with respect to idealized executions, such as linearizability in concurrency. We present a monitoring algorithm incorporating generator-constructed traces, and evaluate it on hyperproperties ranging from security to concurrency, demonstrating that constructed traces not only broaden expressivity but can also significantly accelerate violation detection.

翻译：暂无翻译