guest ::
Deductive reasoning about concurrent probabilistic programs
2025 & 2026
Dissertation, RWTH Aachen University, 2025
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2026
Genehmigende Fakultät
Fak09
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2025-11-05
Online
DOI: 10.18154/RWTH-2026-02088
URL: https://publications.rwth-aachen.de/record/1029086/files/1029086.pdf
Einrichtungen
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
In dieser Dissertation betrachten wir nebenläufige Programme, probabilistische Programme und insbesondere die Kombination beider. Um über nebenläufige Programme zu argumentieren, benutzen wir (klassische) Separationslogik um eine axiomatische Semantik abzuleiten. Separationslogik erlaubtes uns, die Separation von dynamischem Speicher zu deklarieren. Das bedeutet, dass wir ausdrücken können, dass Prädikate an verschiedenen Adressen im dynamischen Speicher gelten können. Wir können also den dynamischen Speicher in Teil-Speicher unterteilen, eines für jeden Prozess und eines das von allen Prozessen genutzt werden kann: den geteilten Speicher. Diese Idee begründet nebenläufige Separationslogik. Für probabilistische Programme benutzen wir eine quantitative Logik. Diese erlaubt es uns eine Abbildung von Zufallsvariablen und einem initialen Zustand des Speichers zu dem Erwartungswert der jeweiligen Zufallsvariable nach Ausführung des probabilistischen Programs im gegebenem Initialzustand zu definieren. Eine quantitative Logik unterscheidet sich von einer klassischen Logik in dem Sinne, dass sie nicht Modelle in Boolesche Werte abbildet, sondern stattdessen in Werte in den reellen Zahlen. Die von uns genutzten quantitative Logiken erlauben außerdem die Benutzung von Separationsoperatoren und bilden damit quantitative Separationslogiken. Mit dieser quantitativen Logik können wir nun axiomatische Semantiken ableiten, die es uns erlaubt eine obere Grenze auf dem Erwartungswert einer Zufallsvariable zu beweisen. Um schließlich über nebenläufige und probabilistische Programme zu argumentieren, kombinieren wir die Techniken um über nebenläufige und über probabilistische Programme zu argumentieren. Wir führen also eine Fuzzy und Separationslogik für nebenläufige und probabilistische Programme ein, indem wir die Ideen von nebenläufige Separation Logic und von quantitativer Separation Logic vereinen. Eine Fuzzylogik bildet Modelle auf reelle Zahlen zwischen null und eins ab. Dies ermöglicht uns eine axiomatische Semantik abzuleiten, mit der wir über untere Grenzen der Wahrscheinlichkeit in einer bestimmten Menge von Zuständen zu terminieren oder nicht zu terminieren argumentieren können. Die Nutzung der vorgestellten axiomatischen Semantiken erfordert es, Implikationen in den entsprechenden Logiken zu beweisen. Eine quantitative oder fuzzy Implikation ist die punktweise Erweiterung der Kleiner-Gleich Relation. Dies stellt jedoch eine Herausforderung dar, da Implikationen in diesen Logiken ohne Restriktionen unentscheidbar sind. Daher betrachten wir eine Technik um über Implikationen in Fuzzy- und Separationslogik zu argumentieren und eine Technik um über Implikationen in quantitativer Separationslogik mit Nutzer-definierten Prädikaten zu argumentieren. Für Implikationen in der Fuzzy- und Separationslogik transformieren wir eine fuzzy Implikation in klassische Separationslogik. Dies erlaubt es uns eine reiche Auswahl an Werkzeugen für klassische Separationslogik zu nutzen. Wir präsentieren eine eingeschränkte Syntax für Fuzzy- und Separationslogik, die es uns erlaubt den fuzzy Anteil automatisch zu lösen, während wir den Separationslogik Teil an ein Programmübergeben, welches Implikationen in Separationslogik beweisen kann. Diese eingeschränkte Syntax erlaubt nur Formeln, deren Semantik eine endliche Wertemenge haben. Die zweite Technik erlaubt es uns Implikationen in der quantitative Separationslogik mit quantitativen Nutzer-definierten Prädikaten zu beweisen. Quantitative Nutzer-definierte Prädikate sind mithilfe von rekursiven Spezifikationen gegeben. Mit diesen können wir sowohl Prädikate die die Form von Datenstrukturen beschreiben, als auch für deren Länge definieren. Um über rekursiv-definierte Prädikate zu argumentieren, benutzen wir zyklische Beweise. Ein zyklischer Beweis erlaubt es uns Rückverbindungen zu vorherigen Beweis-Ausdrücken zu bilden. Solche Beweise sind im Allgemeinen nicht gültig. Daher führen wir eine festgelegte Terminierungsbedingung auf diesen Beweisen ein. Es stellt sich heraus, dass die klassische Terminierungsbedingung, die Ausfaltungen von Prädikaten auf den linken Seiten von Implikationen nutzt, nicht leicht auf quantitative Logiken anwendbar ist. Stattdessen nutzen wir die Größe des dynamischen Speichers als Terminierungsbedingung. In Experimenten scheint diese Terminierungsbedingung kein limitierender Faktor für die Anwendbarkeit des Beweissystems zu sein. Einige Teile dieser Dissertation wurden in der Beweis-Assistenten Sprache Lean geschrieben. Dies erlaubt es uns die formalisierten Beweisregeln zu nutzen, um über nebenläufige und probabilistische Programme in Lean zu argumentieren.In this dissertation, we consider concurrent programs, probabilistic programs and especially the combination of both. To reason about concurrent programs, we facilitate (classical) separation logic to derive axiomatic semantics. Separation logic allows us to declare a separation of heaps. That is, we can declare that predicates hold at different locations in the heap. We can thus partition the heap into a sub-heap used by each thread and a sub-heap used by multiple threads: the shared memory. This idea constitutes concurrent separation logic. For probabilistic programs, we use quantitative logics, which allow us to define a mapping from a random variable and an initial state to the expected value of the respective random variable after executing the given probabilistic program with the given initial state. A quantitative logic differs from a classical logic in that it does not map models to Boolean values, but to real values. Our used quantitative logics also allow for separation operations and thus constitute quantitative separation logics. Using this quantitative logic, we can derive axiomatic semantics to prove an upper bound on the expected value of a random variable. To finally reason about concurrent and probabilistic programs, we combine the techniques to reason about concurrent programs and to reason about probabilistic programs. We thus introduce a fuzzy separation logic for concurrent and probabilistic programs by combining the method to deal with shared memory in concurrent separation logic and the method to deal with expected values in quantitative separation logic. A fuzzy logic maps models to real values between zero and one. This enables us to derive axiomatic semantics to reason about lower bounds of the probability that the program terminates in a certain set of states or does not terminate. The usage of the presented axiomatic semantics requires entailments in the respective logic to be proven. A quantitative or fuzzy entailment is the point-wise lifting of the less-than-or-equals relation. This constitutes a challenge as entailments in the logic without restrictions are undecidable. We thus consider one technique to reason about entailments in fuzzy separation logic and one technique to reason about entailments in quantitative separation logic with user-defined predicates. To reason about entailments in fuzzy separation logic, we transform the entailment into an entailment in classical separation logic. This allows the use of a rich landscape of tools designed for entailments in classical separation logic. We present a restricted syntax which allows the fuzzy part to be solved automatically, while discharging the separation logic part to separation logic entailment checkers. This restricted syntax allows formulae whose semantics has finite image. The second technique allows proving entailments in quantitative separation logic with quantitative user-defined predicates. Quantitative user-defined predicates are given using recursive specifications. With these, we can define predicates that describe the shape for data structures or measure their size. To reason about recursively-defined predicates, we use cyclic proofs. A cyclic proof allows back-linking in proofs to reuse previous proof statements. Such a proof is unsound in general. We introduce a progress criterion on these proofs to guarantee soundness. It turns out that the classic progress criterion using unfoldings of predicates on the left-hand side of the entailment is not easily applicable to quantitative logics. Instead we use heap sizes as our progress criterion. In experiments, the progress criterion does not seem to be a limitation in the applicability of the proof system. Some parts of this dissertation were also formalized in the proof assistant language Lean and thus allow the usage of the formalized proof rules to reason about concurrent and probabilistic programs in Lean.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online
Sprache
English
Externe Identnummern
HBZ: HT031438554
Interne Identnummern
RWTH-2026-02088
Datensatz-ID: 1029086
Beteiligte Länder
Germany
|
The record appears in these collections: |