Skip to main content

Rewriting-Based Runtime Verification for Alternation-Free HyperLTL

Publication Type
Year of Publication
Conference/Journal Name
The 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Page Numbers
Analysis of complex security and privacy policies (e.g., information flow) involves reasoning about multiple execution traces. This stems from the fact that an external observer may gain knowledge about the system through observing and comparing several executions. Monitoring of such policies is in particular challenging because most existing monitoring techniques are limited to the analysis of a single trace at run time. In this paper, we present a rewriting-based technique for runtime
verification of the full alternation-free fragment of HyperLTL, a temporal logic for specification of hyperproperties. The distinguishing feature of our proposed technique is its space complexity, which is independent of the number of trace quantifiers in a given HyperLTL formula.