Lukas Convent

Über Technologie, Naturwissenschaften und Lernen

Kompositionale und Namenslose Formalisierung von HOcore

Betreuer: Tobias Tebbi
Verantwortlich: Prof. Dr. Gert Smolka

Zusammenfassung

Das Hauptaugenmerk dieser Arbeit liegt auf besseren Formalisierungstechniken für den höherstufigen Prozesskalkül HOcore.

HOcore ermöglicht verschiedene Definitionen von Bisimilarität. Diese werden normalerweise kompositionell definiert, jedoch nutzen Beweise über HOcore in der Literatur nicht ihre kompositionale Struktur. Wir betrachten Bisimilarität aus einer koinduktiven Perspektive, der Arbeit von Damien Pous folgend, indem wir seine Formulierung von kompatiblen Funktionen verwenden, um kompositionale Beweise für die Korrektheit von Up-to-Techniken und für Abschlusseigenschaften von Bisimilarität zu erlangen. Da die Abschlussbedingungen einiger Komponenten voneinander abhängen, führen wir das Konzept der bedingten Abgeschlossenheit als Kriterium ein, das auf Bisimilaritäten anwendbar ist, die diese Abhängigkeiten beachten. Durch die Verwendung von de Bruijn-Indizes vermeiden wir Nebenbedingungen zur Disjunktheit freier Variablen. Wir führen Transitionen ein, die für jede unbewachte Variable einen Kontext erzeugen. Auf diese Weise können wir Übergänge substituierter Prozesse elegant analysieren, ohne Verwendung struktureller Kongruenz und ohne separate Behandlung der Wirkungsbereiche von Variablen.

Wir wenden diese Techniken auf HOcore an und zeigen die Korrektheit der Up-to-Bisimilaritätstechnik sowie die Substituierbarkeit und Kongruenz der IO-Bisimilarität. Die resultierende Beweisarchitektur, die im Beweisassistenten Coq formalisiert ist, bietet ein besseres Verständnis der verschiedenen Komponenten und ihrer Abhängigkeiten.

Literatur

B.Sc.-~Abschlussarbeit

Coq-Entwicklung

Präsentationen