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.

GI-FG Meeting (PDF download)

Abstract:

In somewhat informal terms, an unboundedness problem is a decision problem that asks whether there are infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These questions have come into focus in recent years because of their connections to downward closure computation and separability problems. In this talk, we will present general techniques that are both conceptually very simple and applicable to a wide variety of language classes.