Theory Day on Automata and Formal Languages 2026

Original abstract provided for this program:

In recent years, hyperproperties and their specification languages have garnered significant attention within the communities of formal methods, security, and cyber-physical systems.
Hyperproperties relate multiple execution traces within a system and are thereby able to express information-flow properties that capture security and privacy requirements.

HyperLTL is obtained by extending LTL—the most influential specification language for linear-time properties—with trace quantifiers to refer to multiple executions of a system.

HyperLTL model-checking is decidable but computationally expensive. A cheaper (but incomplete) method interprets the verification of a HyperLTL formula as a two-player game between universal and existential quantifiers. This approach is particularly well-suited for producing easily verifiable certificates of satisfaction or violation.

In the first part of the talk, we present the first sound and complete game-based verification algorithm for HyperLTL.
In the second part of the talk, we present ideas on how to scale game-based verification to infinite-state systems.

This talk is based on joint work with Martin Zimmermann.