Logical methods for the hierarchy of hyperlogics

Abstract

In this thesis, we develop logical methods for reasoning about hyperproperties. Hyperproperties describe relations between multiple executions of a system. Unlike trace properties, hyperproperties comprise relational properties like noninterference, symmetry, and robustness. While trace properties have been studied extensively, hyperproperties form a relatively new concept that is far from fully understood. We study the expressiveness of various hyperlogics and develop algorithms for their satisfiability and synthesis problems. In the first part, we explore the landscape of hyperlogics based on temporal logics, first-order and second-order logics, and logics with team semantics. We establish that first-order/second-order and temporal hyperlogics span a hierarchy of expressiveness, whereas team logics constitute a radically different way of specifying hyperproperties. Furthermore, we introduce the notion of temporal safety and liveness, from which we obtain fragments of HyperLTL (the most prominent hyperlogic) with a simpler satisfiability problem. In the second part, we develop logics and algorithms for the synthesis of smart contracts. We introduce two extensions of temporal stream logic to express (hyper)properties of infinite-state systems. We study the realizability problem of these logics and define approximations of the problem in LTL and HyperLTL. Based on these approximations, we develop algorithms to construct smart contracts directly from their specifications.

In dieser Arbeit beschreiben wir logische Methoden, um über Hypereigenschaften zu argumentieren. Hypereigenschaften beschreiben Relationen zwischen mehreren Ausführungen eines Systems. Anders als pfadbasierte Eigenschaften können Hypereigenschaften relationale Eigenschaften wie Symmetrie, Robustheit und die Abwesenheit von Informationsfluss ausdrücken. Während pfadbasierte Eigenschaften in den letzten Jahrzehnten ausführlich erforscht wurden, sind Hypereigenschaften ein relativ neues Konzept, das wir noch nicht vollständig verstehen. Wir untersuchen die Ausdrucksmächtigkeit verschiedener Hyperlogiken und entwickeln ausführbare Algorithmen, um deren Erfüllbarkeits- und Syntheseproblem zu lösen. Im ersten Teil erforschen wir die Landschaft der Hyperlogiken basierend auf temporalen Logiken, Logiken erster und zweiter Ordnung und Logiken mit Teamsemantik. Wir stellen fest, dass temporale Logiken und Logiken erster und zweiter Ordnung eine Hierarchie an Ausdrucksmächtigkeit aufspannen. Teamlogiken hingegen spezifieren Hypereigenschaften auf eine radikal andere Art. Wir führen außerdem das Konzept von temporalen Sicherheits- und Lebendigkeitseigenschaften ein, durch die Fragmente der bedeutensten Logik HyperLTL entstehen, für die das Erfüllbarkeitsproblem einfacher ist. Im zweiten Teil entwickeln wir Logiken und Algorithmen für die Synthese digitaler Verträge. Wir führen zwei Erweiterungen temporaler Stromlogik ein, um (Hyper)eigenschaften in unendlichen Systemen auszudrücken. Wir untersuchen das Realisierungsproblem dieser Logiken und definieren Approximationen des Problems in LTL und HyperLTL. Basierend auf diesen Approximationen entwickeln wir Algorithmen, die digitale Verträge direkt aus einer Spezifikation erstellen.