Theorietag Automaten und Formale Sprachen 2026

Original abstract supplied for this programme:

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

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

HyperLTL model-checking is decidable but 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 how to scale game-based verification to infinite state systems.

This talk is based on joint works with Martin Zimmermann.

Sitzung der GI-FG (pdf-Download)

Abstract:

Somewhat informally, an unboundedness problem is a decision problem that asks about the existence of infinitely many words (satisfying certain properties) in a formal language. For instance: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came 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 at the same time conceptually very simple and also apply to a wide variety of language classes.