💻 computer science

Labelled Process Logic

Diese Arbeit führt ein einheitliches zyklisches etikettiertes beweistheoretisches Framework ein, das aus den Systemen G3PPL und G3FOPL besteht und eine vollständige Behandlung sowohl der propositionale als auch der prädikatenlogischen Prozesslogik erreicht, indem es Formeln mit Etiketten anreichert, um Trace- und Update-Informationen während der Ableitungen explizit zu verfolgen.

Ursprüngliche Autoren: Yuanrui Zhang

Veröffentlicht 2026-06-10

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Yuanrui Zhang

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen zu beweisen, dass ein Roboter niemals abstürzt, während er durch ein Labyrinth navigiert.

In der alten Arbeitsweise (genannt „Dynamische Logik“) prüfte man nur das Ziel des Roboters. Man fragte: „Wenn der Robot hier startet und diesen Anweisungen folgt, wird er dann in der Sicherheitszone ankommen?“ Das ist, als würde man eine Karte erst am Zielort prüfen. Es sagt einem, ob man angekommen ist, aber nicht, ob man auf dem Weg dorthin in einen Abgrund gefahren ist.

Prozesslogik ist ein Upgrade. Sie kümmert sich um die gesamte Reise. Sie fragt: „Ist der Roboter die ganze Zeit auf der Straße geblieben, hat er die Klippen vermieden und bei jedem einzelnen Schritt die Regeln befolgt?“ Dies ist viel schwieriger zu beweisen, da man die gesamte Historie des Roboters verfolgen muss, nicht nur seinen Endpunkt.

Die Arbeit von Yuanrui Zhang führt ein neues, leistungsstarkes Werkzeug namens Labelled Process Logic ein, um dieses schwierige mathematische Problem zu lösen. So funktioniert es, unter Verwendung einfacher Analogien:

1. Das Problem: Der „Splitting“-Albtraum

Stellen Sie sich vor, Sie versuchen zu beweisen, dass ein Roboter sicher durch einen langen Tunnel fahren kann, der aus zwei Abschnitten besteht: Abschnitt A und Abschnitt B.

In traditionellen mathematischen Beweisen muss man oft das Problem „aufteilen“ (splitting), um zu beweisen, dass die gesamte Reise sicher ist. Man versucht zu beweisen, dass Abschnitt A sicher ist, dann zu beweisen, dass Abschnitt B sicher ist, und versucht dann, die beiden Beweise zusammenzukleben.
Das Problem ist, dass der „Kleber“ unordentlich ist. Wenn sich der Pfad des Roboters in Abschnitt A beeinflusst, wie sich Abschnitt B verhält, wird die Mathematik unglaublich kompliziert. Bestehende Werkzeuge konnten einfache Tunnel handhaben, brachen aber zusammen, wenn die Tunnel komplex wurden, sich selbst überlappten oder viele mögliche Pfade hatten.

2. Die Lösung: Der „Rucksack“ (Labels)

Die große Idee des Autors ist es, nicht mehr zu versuchen, die Teile am Ende zusammenzukleben. Stattdessen gibt man dem Beweis einen Rucksack (einen „Label“).

Wie es funktioniert: Während der Beweis durch die Anweisungen des Roboters wandert, schreibt er nicht nur auf: „Ist das sicher?“, sondern: „Wir sind bei Schritt 5, der Roboter ist nach links abgebogen und die Batterie steht bei 80 %.“
Die Magie: Dieser „Rucksack“ (der Label) trägt die Historie der Reise innerhalb des Beweises selbst.
- Anstatt das Problem in zwei schwierige Teile aufzuteilen, fügt der Beweis einfach den neuen Schritt zum Rucksack hinzu.
- Wenn der Roboter Schritt A dann Schritt B macht, aktualisiert der Beweis einfach den Rucksack zu Historie: Schritt A + Schritt B.
- Dies macht die Mathematik viel sauberer. Man braucht keine komplexen Regeln, um Dinge zusammenzukleben; man fügt einfach fortlaufend zur Liste hinzu, was passiert ist.

3. Das Loop-Problem: Der „unendliche Flur“

Computer und Roboter haben oft Schleifen (Loops) (z. B. „Fahre weiter, bis du ein rotes Licht siehst“).

Wenn man versucht, eine Schleife mit Standardmathematik zu beweisen, gerät man vielleicht in einen unendlichen Flur. Man beweist Schritt 1, dann Schritt 2, dann Schritt 3 ... und da sich die Schleife wiederholt, erreicht man das Ende des Beweises nie.
Der zyklische Fix: Der Autor erlaubt dem Beweis, „auf sich selbst zurückzugreifen“. Stellen Sie sich einen Beweis vor, der aussieht wie eine Schlange, die ihren eigenen Schwanz frisst.
- Der Beweis sagt: „Ich bin bei Schritt 10. Ich weiß, dass ich vorhin bei Schritt 1 war. Da die Regeln dieselben sind, kann ich zu Schritt 1 zurückspringen und sagen: ‚Ich habe diesen Teil bereits überprüft, also bin ich auf der sicheren Seite.‘“
- Die Sicherheitsprüfung: Um sicherzustellen, dass dies kein Betrug ist, fügt der Autor eine Regel hinzu: Jedes Mal, wenn der Beweis zurückspringt, muss er beweisen, dass sich der „Rucksack“ (der Label) in einer spezifischen, schrumpfenden Weise verändert hat. Es ist wie ein Spiel, bei dem man nur zurückspringen darf, wenn man weniger Kekse im Glas hat. Irgendwann sind die Kekse auf, was beweist, dass die Schleife sicher und endlich ist.

4. Zwei Versionen des Werkzeugs

Der Artikel baut zwei Versionen dieses Systems auf:

G3PPL (Die einfache Version): Funktioniert für abstrakte Logikrätsel, bei denen es nur um „Wahr“- oder „Falsch“-Zustände geht. Es verwendet Labels, um einfache Pfade zu verfolgen.
G3FOPL (Die fortgeschrittene Version): Funktioniert für die reale Mathematik mit Zahlen und Variablen (wie x = x + 1). Hier verfolgt der „Rucksack“ nicht nur den Pfad, sondern verfolgt Updates. Wenn der Roboter eine Zahl ändert, zeichnet der Label diese Änderung explizit auf (z. B. „x ist jetzt 5“). Dies ermöglicht es dem System, echte Computerprogramme mit Mathematik darin zu handhaben.

Das Fazit

Der Artikel behauptet, das erste vollständige, zuverlässige mathematische Framework entwickelt zu haben, das Eigenschaften über die gesamten Ausführungspfade komplexer Computerprogramme beweisen kann, einschließlich Schleifen und Schleifen mit Mathematik.

Vorher: Konnten wir nur leicht beweisen, wo ein Programm endet, oder konnten sehr einfache Pfade handhaben.
Jetzt: Wir haben ein einheitliches System (unter Verwendung von „Rucksäcken“ und „sicheren Schleifen“), das komplexe, schrittweise Verhaltensweisen sowohl für einfache Logik als auch für komplexe mathematische Programme beweisen kann.

Der Autor beweist, dass dieses System korrekt (Sound – es lügt nie; wenn es sagt, ein Programm sei sicher, dann ist es das auch wirklich) und vollständig (Complete – es kann alles beweisen, was tatsächlich wahr ist) ist. Dies ist ein bedeutender Schritt nach vorn, um sicherzustellen, dass Software exakt so funktioniert, wie wir es erwarten – von der ersten Sekunde bis zur letzten.

Technisches Resümee: Labelled Process Logic

1. Problemstellung

Process Logic (PL) erweitert die Dynamic Logic (DL), indem sie den Fokus von der Argumentation über finale Programmen Zustände hin zur Argumentation über gesamte Ausführungspfade verschiebt. Während die propositionale Theorie der Process Logic (PPL) hinsichtlich Entscheidbarkeit und Vollständigkeit gut verstanden ist, stellt die Erweiterung auf die Prädikatenlogik (First-Order Extension, FOPL) erhebliche Herausforderungen dar.

Die Kernschwierigkeit liegt in der kompositorischen Argumentation, die für die First-Order Process Logic über reguläre Programme erforderlich ist. In der Standard-Dynamic-Logic besagt eine Formel $[\alpha]\phi$ , dass jede terminierende Ausführung von $\alpha$ in einem Zustand endet, der $\phi$ erfüllt. In der Process Logic besagt $[\alpha]\pi$ , dass jede Ausführung eines Pfades von $\alpha$ eine temporale Eigenschaft $\pi$ (ausgedrückt durch Linear Temporal Logic Operatoren wie next, always, eventually und until) erfüllt.

Existierende kompositorische Kalküle für Fragmente dieser Logik (z. B. Beckerts Sequenzenkalkül für deterministische While-Programme oder Erweiterungen wie DLT und DTL) bieten keine vollständige Behandlung für die vollständige First-Order Process Logic über regulären (potenziell nicht-deterministischen) Programmen. Speziell:

Kompositorische Regeln für sequentielle Programme (das Aufteilen einer Pfad-Eigenschaft $\pi$ über $\alpha; \beta$ ) hängen oft stark von der spezifischen Form der temporalen Formel ab (z. B. spezifische Regeln für „always“ vs. „eventually“).
Einige vorgeschlagene Regeln sind für allgemeine reguläre Programme unzureichend, da Tests in sequentiellen Kompositionen Pfade blockieren können, was einfache kompositorische Aufteilungen ungültig macht.
Kein existierendes System bietet ein einheitliches Framework, in dem Pfad-basierte Eigenschaften und First-Order-Berechnungen innerhalb derselben Beweisstruktur behandelt werden.

2. Methodik: Zyklische Labelled Proof Systems

Das Paper schlägt ein neuartiges beweistheoretisches Framework vor, das Process-Logic-Formeln mit Labels anreichert, um Ausführungsinformationen während der Ableitungen explizit aufzuzeichnen, anstatt sich auf zunehmend komplexere kompositorische Regeln zu verlassen.

2.1 Labelled Formulas

Die Autoren führen gelabelte Formeln der Form $\sigma : \phi$ ein, wobei:

$\phi$ eine Process-Logic-Formel ist.
$\sigma$ $σ$ ein Label ist, das die bisher akkumulierte Ausführung oder Programkonfiguration darstellt.
- In der Propositional Process Logic (PPL) sind Labels Pfade von Welten ( $\sigma \in L$ ), konstruiert aus Welt-Variablen, Pfad-Variablen und Konkatenation.
- In der First-Order Process Logic (FOPL) sind Labels um Program Updates ( $U$ ) erweitert, um den kumulativen Effekt von Zuweisungen (z. B. $\{u := e\}$ ) über eine arithmetische Struktur aufzuzeichnen.

Dieser Ansatz macht Zwischeninformationen der Ausführung innerhalb des Beweissystems verfügbar. Folglich muss das Beweissystem sequentielle Pfade nicht mehr mittels spezieller temporaler Regeln am Punkt der Sequenz aufteilen; stattdessen entfaltet es die Programmenstruktur, während es Informationen im Label akkumuliert.

2.2 Zyklische Beweisstruktur

Da reguläre Programme Iterationen ( $\alpha^*$ ) beinhalten, kann die Beweissuche zyklische Ableitungen generieren. Um dies zu handhaben, verwenden die Autoren die zyklische Beweistheorie.

Preproofs: Endliche Bäume, bei denen die Blattknoten („Buds“) zu Vorfahrenknoten mit identischer syntaktischer Form (modulo Variablenumbennung) „zurückverlinken“ können.
Zyklische Bedingung: Um die Korrektheit (Soundness) zu gewährleisten, sind nicht alle Zyklen gültig. Das Paper definiert eine progressive Ableitungsspur. Eine Ableitung ist ein gültiger zyklischer Beweis, wenn jeder unendliche Pfad einen „progressiven Schritt“ enthält (z. B. Anwendung einer Regel, die die Komplexität des Labels oder der Formel reduziert).
Soundness-Mechanismus: Die Autoren beweisen die Korrektheit, indem sie zeigen, dass jede unendliche Ableitung, die die zyklische Bedingung erfüllt, eine unendliche Deszendenz in einer wohlgeordneten Multimengen-Ordnung von „minimalen Gegenbeispiel-Pfaden“ induziert. Dieser Widerspruch stellt sicher, dass keine ungültige Formel bewiesen werden kann.

2.3 Die Beweissysteme

Es werden zwei spezifische Systeme definiert:

G3PPL: Ein zyklisches gelabeltes Beweissystem für die Propositional Process Logic. Es erweitert gelabelte Sequenzen-Techniken für Modallogiken und passt diese an Pfad-Semantiken an.
G3FOPL: Ein zyklisches gelabeltes Beweissystem für die First-Order Process Logic. Es erweitert G3PPL durch Ersetzung atomarer Programmen-Regeln durch Regeln für Zuweisungen (Update des Labels) und das Hinzufügen von Standard-First-Order-Quantor-Regeln.

3. Zentrale Beiträge

Das Paper leistet folgende spezifische Beiträge:

Labelled Formulas: Die Einführung von Pfad-Labels für PPL und Update-basierten Labels für FOPL, was es ermöglicht, die Ausführungsgeschichte innerhalb der Beweisstruktur explizit zu verfolgen.
Zyklische Gelabelte Systeme: Die Definition von G3PPL und G3FOPL, die ein gemeinsames gelabeltes Framework nutzen, aber jeweils spezifische Regeln für die Propositional bzw. First-Order Process Logic verwenden.
Korrektheitsbeweise (Soundness): Ein Beweis der Korrektheit für beide Systeme. Das Argument stützt sich auf die Reduktion jeder progressiven unendlichen Ableitung auf eine unendliche Deszendenz in einer wohlgeordneten Multimengen-Ordnung minimaler Gegenbeispiel-Pfade.
Vollständigkeitsbeweise (Completeness):
- Für G3PPL wird die Vollständigkeit dadurch etabliert, dass das gelabelte System jedes Axiom und jede Regel des etablierten Hilbert-artigen Beweissystems für PPL ableiten kann.
- Für G3FOPL wird die Vollständigkeit durch die Anpassung des klassischen Vollständigkeitsarguments für die First-Order Dynamic Logic (FODL) an das Pfad-basierte Setting unter Verwendung arithmetischer Kodierungen etabliert.

4. Ergebnisse

Einheitliches Framework: Das Paper konstruiert erfolgreich ein einheitliches Framework, in dem Pfad-basierte Programmeigenschaften und First-Order-Berechnungen innerhalb derselben Beweisstruktur gehandhabt werden.
Vollständigkeit für reguläre Programme: Die Systeme bieten das erste vollständige logische Framework für die vollständige First-Order Process Logic über regulären Programmen (einschließlich Nicht-Determinismus und Iteration).
Korrektheit und Vollständigkeit: Sowohl G3PPL als auch G3FOPL sind im Hinblick auf ihre jeweilige Semantik als korrekt und vollständig bewiesen.

5. Bedeutung

Das Paper behauptet, dass diese Arbeit eine langjährige Lücke in der Literatur schließt. Vorherige Systeme waren entweder:

Auf deterministische Programme beschränkt (z. B. DLT, DTL).
Unvollständig für allgemeine reguläre Programme.
Nicht in der Lage, alle LTL-Operatoren (z. B. until) in Anwesenheit von Nicht-Determinismus einheitlich zu behandeln.

Durch die Verwendung von Labels, um Ausführungsinformationen zu externalisieren, und zyklischer Beweise zur Handhabung von Iterationen, bieten die Autoren einen prinzipienbasierten und einheitlichen Mechanismus für die Argumentation über Pfad-Eigenschaften. Dies ermöglicht die Verifikation von Spezifikationen, bei denen das Zwischenverhalten essenziell ist, ohne dass ad-hoc-kompositorische Regeln für jeden temporalen Operator erforderlich sind. Das Framework vereinheitlicht die Behandlung der propositionalen und der First-Order-Ebene und bietet eine robuste Grundlage für die Programmverifikation unter Einbeziehung komplexer temporaler Eigenschaften.