Hyperproperties as Design Principles: Information-Flow Guided Synthesis and Explainability in Distributed Systems

Bernd Finkbeiner
CISPA Helmholtz Center for Information Security and Technical University of Munich

Information flow is central to the design of distributed and multi-agent systems, and its formal analysis naturally leads to hyperproperties – requirements over sets of executions. This talk presents two developments that use hyperproperties to address core challenges in synthesis and verification. First, we introduce information-flow assumptions, which capture the epistemic requirements a specification imposes on components in a distributed system. Unlike traditional behavioral assumptions, they characterize which information must be available rather than how it is produced. This yields a new compositional approach to distributed synthesis. Second, we discuss the specification and verification of explainability, understood as a positive information-flow requirement ensuring that agents can know why certain effects occur. Using epistemic temporal logic enriched with counterfactual reasoning, we obtain expressive system-level specifications that interact naturally with privacy constraints. Together, these results illustrate how hyperproperties offer a unifying foundation for designing and analyzing trustworthy distributed and multi-agent systems.