2025-11-15T12:40:11.869613

Formally Verified Certification of Unsolvability of Temporal Planning Problems

Wang, Abdulaziz
We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.
academic

Formal verifizierte Zertifizierung der Unlösbarkeit von zeitlichen Planungsproblemen

Grundinformationen

  • Paper-ID: 2510.10189
  • Titel: Formally Verified Certification of Unsolvability of Temporal Planning Problems
  • Autoren: David Wang, Mohammad Abdulaziz (King's College London, Vereinigtes Königreich)
  • Klassifizierung: cs.LO (Logik in der Informatik), cs.AI (Künstliche Intelligenz)
  • Veröffentlichungsdatum: 11. Oktober 2025 (arXiv-Preprint)
  • Paper-Link: https://arxiv.org/abs/2510.10189

Zusammenfassung

In diesem Artikel wird eine Methode zur Zertifizierung der Unlösbarkeit von zeitlichen Planungsproblemen vorgestellt. Die Methode basiert auf der Kodierung von Planungsproblemen als Netzwerke von Zeitautomaten und der anschließenden Verwendung eines effizienten Modellprüfers sowie eines Zertifikatsprüfers zur Zertifizierung der Ausgabe des Modellprüfers. Die Methode priorisiert die Vertrauenswürdigkeit der Zertifizierung: Die Implementierung der Kodierung von Zeitautomaten wird mit dem Theorembeweiser Isabelle/HOL formal verifiziert, und ein bestehender Zertifikatsprüfer (ebenfalls formal verifiziert in Isabelle/HOL) wird zur Zertifizierung der Modellprüfungsergebnisse verwendet.

Forschungshintergrund und Motivation

Kernproblem

Das Kernproblem dieser Forschung ist die Zertifizierung der Unlösbarkeit von zeitlichen Planungsproblemen. Zeitliche Planung ist eine reichhaltige Planungsform, die es Aktionen ermöglicht, Dauern zu haben und gleichzeitig ausgeführt zu werden, was komplexer ist als klassische Planung.

Bedeutung des Problems

  1. Anforderungen an Vertrauenswürdigkeit: Bestehende Planungssysteme sind auf algorithmischer und Implementierungsebene äußerst komplex; die Verbesserung der Vertrauenswürdigkeit ihrer Ausgaben ist von entscheidender Bedeutung
  2. Schwierigkeit der Zertifizierung: Im Gegensatz zu lösbaren Problemen (die durch Ausführung eines Plans verifiziert werden können) sind Aussagen über Unlösbarkeit oder Optimalität schwer zu kompakten Zertifikaten zu erhalten
  3. Exponentielle Komplexität: Im schlimmsten Fall können solche Zertifikate exponentiell in Bezug auf die Größe der Planungsaufgabe wachsen

Einschränkungen bestehender Methoden

  1. Mangel an formalen Garantien: Bestehende Methoden zur Erkennung der Unlösbarkeit zeitlicher Planung bieten keine formalen Korrektheitszusicherungen
  2. Hohe Komplexität: Die fortschrittlichsten Techniken der zeitlichen Planung sind sehr komplex und erschweren die Entwicklung praktischer Unlösbarkeits-Zertifizierungsschemata
  3. Verifikationslücke: Im Vergleich zu bereits durchgeführten formalen Verifikationsarbeiten in der klassischen Planung besteht in der zeitlichen Planung eine Lücke

Forschungsmotivation

Dieser Artikel verfolgt einen Kodierungs-Transformations-Ansatz: Zeitliche Planungsprobleme werden in andere Rechenproblemen kodiert, für die bereits praktische Zertifizierungsalgorithmen existieren (Zeitautomaten), und der gesamte Kodierungsprozess und der Zertifikatsprüfer werden durch einen Theorembeweiser formal verifiziert, um die Vertrauenswürdigkeit der Zertifizierung zu gewährleisten.

Kernbeiträge

  1. Formal verifizierte Kodierungsmethode: Erstmalige formale Verifikation der Kodierung zeitlicher Planung in Zeitautomaten von Heinz et al.
  2. Technische Implementierung: Anpassung der Kodierung zur Erzeugung von Zeitautomaten-Formaten, die mit dem System von Wimmer und von Mutius kompatibel sind
  3. Vereinfachte Semantik-Gestaltung: Entwurf einer einfacheren Semantik für zeitliche Planung als bestehende Arbeiten, die mathematische Überlegungen erleichtert, mit Beweis der Äquivalenz zu bestehenden Semantiken
  4. Vollständiges Zertifizierungsframework: Aufbau einer vollständigen vertrauenswürdigen Zertifizierungskette von zeitlichen Planungsproblemen zu Zeitautomaten-Modellprüfung
  5. Theoretische Korrektheitszusicherung: Beweis der Korrektheit der Kodierung in Isabelle/HOL mit starken theoretischen Garantien

Methodische Details

Aufgabendefinition

Eingabe: Zeitliches Planungsproblem P = ⟨P, A, I, G⟩

  • P: Menge von Propositionen
  • A: Menge von Aktionen mit Dauer
  • I: Initialzustand
  • G: Zielzustand

Ausgabe: Formales Zertifikat der Unlösbarkeit (falls das Problem tatsächlich unlösbar ist)

Einschränkungen:

  • Aktionen haben Start- und End-Snapshot-Aktionen
  • Unterstützung für Invarianten und Planungsbeschränkungen
  • Erfüllung von gegenseitigen Ausschluss- und Dauerbegrenzungen

Modellarchitektur

1. Formalisierung der zeitlichen Planung

Der Artikel definiert zunächst die formale Semantik der zeitlichen Planung:

Snapshot-Aktionen (Definition 1):

h ≡ ⟨pre(h), adds(h), dels(h)⟩

Aktionen mit Dauer (Definition 2):

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

wobei a⊢ und a⊣ jeweils die Start- und End-Snapshot-Aktionen sind.

2. Kodierung von Zeitautomaten

Variablengestaltung (Definition 24):

  • Für jede Proposition p: Binärvariable vp (kodiert Wahrheitswert) und Sperrzähler lp (verfolgt aktive Aktionen, die p wahr benötigen)
  • aa: Gesamtzahl aktiver Aktionen
  • ps: Planungszustand (0=nicht gestartet, 1=läuft, 2=abgeschlossen)

Uhrengestaltung (Definition 25):

  • Jeder Aktion a werden zwei Uhren zugeordnet: ca⊢ (verfolgt Zeit nach Start) und ca⊣ (verfolgt Zeit nach Ende)

Hauptautomat (Definition 26): Steuert die Zustandsübergänge des gesamten Planungsprozesses, einschließlich Initialisierung und Zielprüfung.

Aktionsautomaten (Definition 27): Jede Aktion entspricht einem Automaten mit folgenden Schlüsselübergängen:

  • sea: Anwendung der Startaktionseffekte
  • se'a: Sperrung von Invarianten
  • eea: Vorbereitung vor Ende
  • ee'a: Anwendung der Endaktionseffekte
  • iea: Verarbeitung momentaner Aktionen

3. Netzwerk-Konstruktion

Kombination des Hauptautomaten und aller Aktionsautomaten zu einem Zeitautomaten-Netzwerk (Definition 28), wobei die Anfangskonfiguration alle Automaten im inaktiven Zustand setzt.

Technische Innovationen

  1. Unterstützung für gleichzeitige Ausführung: Im Gegensatz zu Heinz et al., die globale Sperren verwenden, ermöglicht dieser Artikel die gleichzeitige Ausführung von Snapshot-Aktionen durch Uhren-Beschränkungen
  2. Verarbeitung momentaner Aktionen: Unterstützung für Aktionen mit Null-Dauer durch Hinzufügen von iea-Übergängen
  3. Formale Verifikation: Erstmalige Bereitstellung von maschinengeprüften Korrektheitsnachweisen für solche Kodierungen
  4. Semantik-Vereinfachung: Entwurf einer für formale Überlegungen besser geeigneten Semantik der zeitlichen Planung

Experimentelle Einrichtung

Formale Verifikationsumgebung

  • Theorembeweiser: Isabelle/HOL
  • Zertifikatsprüfer: Verifizierter Zertifikatsprüfer von Wimmer und von Mutius
  • Zielproperschaft: Erreichbarkeitsprüfung A ⊨ EF(loc(AM) = goal)

Codeumfang-Statistiken

KomponenteCodezeilen
Formalisierung abstrakter zeitlicher Planungssemantik~7.200
Zeitautomaten-Netzwerk-Definition mit Munta~800
Beweis von Theorem 1 und verwandten Lemmata~8.500
Listenbezogene Lemmata~1.500
Gesamt~18.000

Vergleichende Benchmarks

Größenvergleich mit verwandten formalen Arbeiten:

  • Verifizierter SAT-basierter Planer: ~17.500 Zeilen
  • Verifizierter klassischer Planungsverifizierer: ~3.000 Zeilen
  • Verifizierter zeitlicher PDDL-Planungsverifizierer: ~6.500 Zeilen

Experimentelle Ergebnisse

Haupttheoretische Ergebnisse

Theorem 1 (Hauptkorrektheitssatz): Wenn ein Plan π gültig und selbstüberlappungsfrei ist (valid(π) ∧ no_self_overlap(π)), dann gilt die Aussage A ⊨ EF(loc(AM) = goal).

Beweisstruktur:

  1. Lemma 1: Konstruktion einer Simulation, die parallele Pläne induziert
  2. Lemma 2: Erreichbarkeit von der Anfangskonfiguration zum kodierten Zustand
  3. Lemma 3: Übergänge vom Endzustand zur Zielkonfiguration

Formale Verifikationsergebnisse

  1. Vollständigkeitsbeweis: Erfolgreicher Beweis der Vollständigkeit der Kodierung, d.h. jeder gültige Plan findet eine gültige Ausführung im entsprechenden Zeitautomaten-Netzwerk
  2. Maschinenprüfung: Alle Beweise werden durch Isabelle/HOL maschinengeprüft und bieten das höchste Vertrauensniveau
  3. Modularer Entwurf: Beweisstruktur ist modular aufgebaut für leichte Verständlichkeit und Wartbarkeit

Verifikation der technischen Implementierung

Die Kodierungsimplementierung wurde an das Format des bestehenden verifizierten Zertifikatsprüfers angepasst und bildet eine vollständige ausführbare Zertifizierungskette.

Verwandte Arbeiten

Zertifizierung in der klassischen Planung

  • Eriksson et al. entwickelten kompakte Unlösbarkeits-Zertifizierungsschemata für klassische Planung
  • Abdulaziz und Lammich stellten einen formal verifizierten Verifizierer für klassische Planung bereit

Zeitliche Planung und Modellprüfung

  • Dierks et al. implementierten statische Reduktion von PDDL-Teilmengen zu Zeitautomaten
  • Heinz et al. definierten explizite Kodierungen von zeitlichen Planungsproblemen zu Zeitautomaten
  • Gigante et al. untersuchten die Komplexität zeitlicher Planung auf theoretischer Ebene

Formale Verifikationsmethoden

  • Abdulaziz und Kurz entwickelten mit ähnlichen Methoden ein zertifiziertes SAT-basiertes Planungssystem
  • Kumar et al. und Leroy verwendeten schrittweise Verifikation von Kodierungen in der Compiler-Verifikation

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

  1. Machbarkeitsprüfung: Nachweis, dass formale Zertifizierung der Unlösbarkeit zeitlicher Planung machbar ist
  2. Theoretische Garantien: Starke Korrektheitszusicherungen durch Theorembeweiser
  3. Technische Implementierung: Erfolgreicher Aufbau einer vollständigen Zertifizierungswerkzeugkette

Einschränkungen

  1. Eingabebeschränkungen: Aktuell werden nur bereits instanziierte zeitliche Planungsprobleme akzeptiert
  2. Semantik-Teilmenge: Die unterstützte Semantik ist eine Teilmenge des verifizierten Planungsverifizierers
  3. Ausführbarkeit: Der Zertifizierungsmechanismus ist noch nicht vollständig ausführbar

Zukünftige Richtungen

  1. Äquivalenzbeweis: Geplanter formaler Beweis der Äquivalenz zwischen der Semantik dieses Artikels und bestehenden Verifizierer-Semantiken
  2. Ausführbare Implementierung: Entwicklung eines ausführbaren Zertifikatsprüfers
  3. Instanziierungsverifikation: Formale Verifikation von Instanziierungsalgorithmen wie Helmerts Datalog-Solver
  4. Entspannung von Beschränkungen: Untersuchung der Möglichkeit, die Bedingung der Selbstüberlappungsfreiheit zu lockern

Tiefgehende Bewertung

Stärken

  1. Theoretische Strenge: Erstmalige maschinengeprüfte formale Beweise für die Zertifizierung der Unlösbarkeit zeitlicher Planung
  2. Technische Vollständigkeit: Nicht nur theoretisches Framework, sondern auch Integration mit bestehenden Werkzeugen
  3. Methodische Innovation:
    • Kodierungsgestaltung mit Unterstützung für gleichzeitige Ausführung
    • Elegante Lösung für die Verarbeitung momentarer Aktionen
    • Vereinfachte und äquivalente Semantik-Gestaltung
  4. Vertrauenswürdigkeit: Höchstes Niveau der Korrektheitszusicherung durch Theorembeweiser

Schwächen

  1. Praktische Einschränkungen:
    • Erfordert vorinstanziierte Eingaben
    • Noch nicht vollständig ausführbar
    • Fehlende Leistungsbewertung
  2. Abdeckungsbereich: Unterstützt nur eine Teilmenge der zeitlichen Planung, nicht vollständige PDDL-Funktionen
  3. Skalierbarkeit: Der Umfang von 18.000 Codezeilen für formale Arbeiten ist beträchtlich mit hohen Wartungskosten

Auswirkungen

  1. Akademische Beiträge:
    • Schließt die Lücke in der formalen Verifikation zeitlicher Planung
    • Bietet neue theoretische Grundlagen für Unlösbarkeits-Zertifizierung
    • Demonstriert die Machbarkeit der formalen Verifikation komplexer Systeme
  2. Praktischer Wert:
    • Bietet vertrauenswürdige Zertifizierung von Planungssystemen für kritische Anwendungen
    • Erweiterbar auf andere Planungsformen und Constraint-Satisfaction-Probleme
    • Bietet Referenzen für die Entwicklung automatisierter Verifikationswerkzeuge
  3. Reproduzierbarkeit: Basierend auf Open-Source Isabelle/HOL, theoretisch vollständig reproduzierbar

Anwendungsszenarien

  1. Kritische Systeme: Planungsanwendungen, die hohe Vertrauenswürdigkeit erfordern (z.B. Luft- und Raumfahrt, medizinische Geräte)
  2. Forschungswerkzeuge: Bereitstellung von Infrastruktur für formale Verifikation in der zeitlichen Planungsforschung
  3. Bildungszwecke: Als Fallstudie für formale Methoden und Planungsalgorithmen-Lehre
  4. Werkzeugentwicklung: Theoretische Grundlagen für die Entwicklung vertrauenswürdiger Planungswerkzeuge

Literaturverzeichnis

Wichtige Referenzen umfassen:

  • Abdulaziz & Koller (2022): Formale Semantik und Verifizierer für zeitliche Planung
  • Heinz et al. (2019): Kodierung zeitlicher Planung in Zeitautomaten
  • Wimmer & von Mutius (2020): Verifizierter Zertifikatsprüfer für Zeitautomaten
  • Abdulaziz & Kurz (2023): Verifiziertes SAT-basiertes Planungssystem

Dieser Artikel leistet wichtige Beiträge im Bereich der formalen Verifikation zeitlicher Planung. Obwohl es noch Verbesserungspotenzial in Bezug auf praktische Anwendbarkeit gibt, legen seine theoretische Strenge und methodische Innovation eine solide Grundlage für die Entwicklung dieses Forschungsbereichs.