On Propositional Dynamic Logic and Concurrency

1. Problemstellung

Die Propositionale Dynamische Logik (PDL) ist ein mächtiges Werkzeug zur formalen Verifikation von Programmen, bei dem Programme durch Modaloperatoren ($[\alpha]\phi$ und $\langle\alpha\rangle\phi$) in die Logik integriert werden. Traditionell werden Programme in der PDL durch reguläre Ausdrücke repräsentiert, die als Elemente einer Kleene-Algebra behandelt werden. Die Semantik basiert dabei auf der Menge der möglichen Ausführungstraces (Folgen von Aktionen).

Das zentrale Problem bei der Anwendung der PDL auf nebenläufige Systeme (Concurrency) liegt in der Modellierung von Interleaving (Verschachtelung von Aktionen paralleler Prozesse):

• In sequentiellen Programmen entspricht die logische Äquivalenz der Trace-Äquivalenz.
• Bei nebenläufigen Programmen müssen Traces, die sich nur durch die Reihenfolge unabhängiger Aktionen unterscheiden (Kommutativität, z. B. $\alpha; \beta = \beta; \alpha$), als äquivalent betrachtet werden.
• Das Wortproblem für Kleene-Algebren, die um solche Kommutativitätsaxiome erweitert sind, ist jedoch unentscheidbar.
• Dies führt dazu, dass die Gleichheit zweier Modaloperatoren in der PDL nicht entscheidbar ist, sobald Interleaving involviert ist.
• Bestehende Ansätze zur Erweiterung der PDL für Nebenläufigkeit (z. B. Concurrent PDL) sind oft unvollständig, unterstützen keine rekursiven Definitionen oder können komplexe Modelle wie den $\pi$-Kalkül oder Choreographien nicht adäquat abbilden.

2. Methodik: Operational Propositional Dynamic Logic (OPDL)

Die Autoren schlagen einen Paradigmenwechsel vor: Sie trennen die Programme von ihren Traces. Statt Programme direkt als Elemente einer Algebra zu behandeln, wird eine operationale Semantik als Parameter eingeführt.

• Trennung von Syntax und Semantik: Programme werden durch eine Menge $P$ und eine operationale Semantik $O$ (eine labelierte Übergangsrelation $P \times L \times P$) definiert. Die Traces werden nicht im Logikkalkül selbst konstruiert, sondern durch die Semantik generiert.
• Operationaler Axiom: Die Logik wird um ein neues Axiom erweitert, das die operationale Semantik in die Trace-Logik integriert:
  $$[\alpha]\phi \iff \bigvee_{\alpha \xrightarrow{\beta} \gamma} [\beta][\gamma]\phi$$
  Dieses Axiom (AO) zerlegt ein Programm $\alpha$ basierend auf seinen möglichen ersten Schritten ($\beta$) und dem Restprogramm ($\gamma$).
• Sequentkalkül: Die Autoren definieren einen nicht-wellfoundeden Sequentkalkül (unendliche Beweise sind erlaubt, solange sie bestimmte Fortschrittsbedingungen erfüllen), der auf dem System $LPD$ aus der Literatur aufbaut, aber um Regeln zur Handhabung der operationalen Semantik erweitert wird ($[O]$ und $\langle O\rangle$).

3. Schlüsselbeiträge

1. Einführung von OPDL: Ein allgemeines Framework, das PDL parametrisiert durch die operationale Semantik der betrachteten Programme. Dies ermöglicht die Anwendung auf beliebige Programmiersprachen und Semantiken (z. B. CCS, Choreographien).
2. Cut-Eliminierung für nicht-wellfoundede Kalküle: Der erste Beweis der Cut-Eliminierung für einen endlich verzweigenden, nicht-wellfoundeden Sequentkalkül für PDL.
   • Da der Kalkül unendliche Beweise zulässt (für Rekursion), ist die Standard-Cut-Eliminierung nicht konfluent.
   • Die Autoren entwickeln deterministische Cut-Eliminierungs-Strategien und nutzen die Theorie der Scott-Domänen, um zu zeigen, dass der Grenzwert einer Folge von Approximationen eine wohldefinierte, cut-freie und fortschreitende (progressing) Ableitung ist.
3. Vollständigkeit und Korrektheit:
   • Beweis der Korrektheit und Vollständigkeit von OPDL bezüglich der operationalen Semantik.
   • Nachweis, dass logische Äquivalenz in OPDL exakt der Trace-Äquivalenz der zugrundeliegenden operationalen Semantik entspricht.
4. Anwendungsfälle:
   • CCS (Calculus of Communicating Systems): Modellierung von Parallelität durch explizite Parallelkomposition und Interleaving.
   • Choreographic Programming: Modellierung von Nebenläufigkeit durch Out-of-Order-Ausführung unabhängiger Anweisungen (ohne expliziten Paralleloperator, sondern durch Verzögerung von Anweisungen in sequentiellen Choreographien).

4. Ergebnisse

• Ausdrucksstärke: OPDL kann Programme mit Rekursion, Parallelität und Out-of-Order-Ausführung behandeln, was mit klassischer PDL aufgrund der Unentscheidbarkeit des Wortproblems in Kleene-Algebren mit Kommutativität nicht möglich war.
• Wiederverwendbarkeit: Das Framework fasst frühere Arbeiten (z. B. PDL für CCS*, $\pi$-DL, APDL) als spezielle Instanzen zusammen.
• Beweisbarkeit komplexer Äquivalenzen: Die Autoren demonstrieren, dass bekannte Äquivalenzen (z. B. Distributivität von Prefix über Wahl, Kommutativität von Parallelität, Austauschgesetz von Sequentialität und Parallelität) innerhalb des Systems bewiesen werden können, ohne die Semantik jedes Mal neu zu analysieren.
• Beispiel CCS: Es wird gezeigt, dass zwei Prozesse, die trace-äquivalent, aber nicht bisimilar sind (z. B. $(\alpha.\beta.\pi_1) + (\alpha.\gamma)$ vs. $\alpha.(\beta.\pi_2 + \gamma)$), in OPDL als logisch äquivalent bewiesen werden können.
• Beispiel Choreographien: Die Fähigkeit, Out-of-Order-Ausführung zu modellieren, erlaubt die korrekte Behandlung von Choreographien, bei denen unabhängige Aktionen parallelisiert werden können, obwohl sie syntaktisch sequentiell geschrieben sind.

5. Bedeutung und Ausblick

Die Arbeit ist von großer Bedeutung für die formale Verifikation nebenläufiger Systeme:

• Brückenschlag: Sie überbrückt die Lücke zwischen der algebraischen Behandlung von Programmen (Kleene-Algebren) und der operationalen Semantik (LTS), die in der Prozessalgebra üblich ist.
• Flexibilität: Da OPDL parametrisiert ist, kann es leicht an neue Programmierparadigmen oder Semantik-Regeln angepasst werden, ohne die gesamte Logik neu zu erfinden.
• Zukünftige Forschung:
  • Untersuchung des Entscheidungsproblems (Entscheidbarkeit) für verschiedene Instanzen von OPDL, da die Fisher-Ladner-Abschließung bei nicht-regulären Programmen unendlich sein kann.
  • Erweiterung auf den $\pi$-Kalkül (dynamische Namensübertragung).
  • Anwendung auf die Korrektheitsbeweise für Endpoint Projection in choreographischen Sprachen.
  • Integration in algebraische Ansätze (z. B. Erweiterung von Kleene-Algebren um operationale Semantik).

Zusammenfassend bietet OPDL ein robustes, theoretisch fundiertes und praktisch anwendbares Framework, das die Grenzen der klassischen PDL in Bezug auf Nebenläufigkeit überwindet und eine einheitliche Basis für die logische Analyse komplexer verteilter Systeme schafft.