Workshop im Rahmen des Graduiertenkollegs

”Spezifikation diskreter Prozesse und Prozeßsysteme durch operationelle Modelle und Logiken“

vom 17.2.97 bis 21.2.97

in Reinhardtsdorf / Sächsische Schweiz

Teilnehmerliste: Dipl.-Inf. Sven–Erik Bornscheuer, Prof. Dr. rer. nat. habil. Manfred Droste, Prof. Dr. rer. nat. habil. Steffen Hölldobler, Dipl.-Inf. Daniel Kirsten, Dipl.-Inf. Armin Kühnemann, Dipl.-Math. Ralph Kummetz, Dr. rer. nat. Dietrich Kuske, Dipl.-Inf. Helko Lehmann, Dipl.- Inf. Markus Lohrey, Dr. rer. nat. Walter Nauber, Prof. Dr. rer. nat. habil. Reinhard Pöschel, Dr. rer. nat. habil. Michael Posegga, Prof. Dr. rer. nat. habil. Horst Reichel, Martin Rößiger, Dmitri Schamschurko, Dr. rer. nat. Karsten Schmidt, Hans–Peter Störr, Dipl.-Inf. Hendrik Tews, M. Sc. Christian Urban, Prof. Dr.–Ing. habil. Heiko Vogler

\underline{Zeitplan:}

Tag  Uhrzeit  Vortragender  Thema
Montag, 17.2.  9.30 – 9.45  — Begrüßung —
9.45 – 11.00  Droste  Automaten und Logik
11.30 – 12.30  ”  Automaten mit Nebenläufigkeitsrelation
14.00 – 16.00  Pöschel  Funktionen und Relationen
16.30 – 17.30  ”  ”
17.45 – 18.45  Kuske  Temporale Logiken für Spuren
Dienstag, 18.2.  9.00 – 11.00  Reichel  Spezifikation von PADT’s
11.30 – 12.30  ”  Verhaltenssemantik / Coalgebren
14.15 – 16.00  Vogler  Funktional–logische Programmierung
16.30 – 17.45  ”  Baumübersetzer,

Attributgrammatiken und Logikprogramme

Mittwoch, 19.2. 9.00 – 13.00 — Exkursion —
14.30 – 16.00 Hölldobler  Resolution und Unifikation
16.30 – 18.15  ”  Fluent–Kalkül
Donnerstag, 20.2. 9.00 – 10.00  Schmidt  Symmetrien in Petrinetzen
10.00 – 11.00  ”  Analyse algebraischer Petrinetze
11.30 – 12.30 Bornscheuer  Parakonsistente Modellierung

gleichzeitiger Aktionen

14.00 – 15.00 Lehmann  Aktionen, Bedingungen, Ressourcen
15.00 – 16.10  Droste  Automaten mit Nebenläufigkeitsrelation
16.40 – 17.40  Lohrey  Ressourcenbasierte Modelle
Freitag, 21.2.  9.00 – 11.00  Urban  Normalisierung und Cut–Eliminierung
11.30 – 12.30  — Diskussion über Lehrveranstaltungen —

— im SS 97 und WS 97/98 — Inhalt der Vorträge: Manfred Droste: Automaten und Logik / Automaten mit Nebenläufigkeitsrelation Im ersten Teil dieses Vortrags wurde zunächst das Konzept der endlichen Automaten zu dem Konzept der M–Automaten für beliebige Monoide verallgemeinert. Weiterhin wurde das Resultat von Büchi erläutert, nach dem die Klasse der von M–Automaten erkannten Sprachen gleich der Klasse der Sprachen ist, die in der monadischen Logik zweiter Stufe definierbar sind. Im zweiten Teil des Vortrags wurden Automaten mit Nebenläufigkeitsrelationen definiert und deren Zusammenhang zu Platz/Transitions–Netzen beschrieben. Weiterhin wurde eine Beziehung zur Theorie der Spuren geknüpft.

Reinhard Pöschel: Vollständigkeitsproblem / Klone / Galoisverbindung Es wurden einige Fragestellungen aus der universellen Algebra wie z.B. das Vollständigkeitsproblem für eine Menge von Operationen auf einer Menge diskutiert. Zu diesem Zweck wurden zunächst mehrere zentrale Begriffe wie z.B. Funktionen- bzw. Relationenklones, Polymorphismen von Relationen sowie die Invarianz von Relationen definiert. Zwischen diesen Begriffen wurde eine Galoisverbindung hergestellt, die dann auf einige der anfangs diskutierten Fragestellungen angewendet wurde.

Dietrich Kuske: Temporale Logiken für Spuren Ein Vorläufer der in diesem Vortrag vorgestellten temporalen Logik linearer Zeit für Spuren (Mazurkiewicz traces) ist von Ebinger 1994 eingeführt worden. Dabei zeigte er, daß diese Logik für endliche Spuren ebenso ausdrucksstark ist wie die Prädikatenlogik erster Stufe. Herr Kuske berichtete von einer Erweiterung der Ebingerschen Logik um Quantoren; die resultierende Logik ist gleich ausdrucksstark wie die monadische Logik zweiter Stufe für endliche und unendliche Spuren und damit entscheidbar. Außerdem charakterisierte er ein Fragment dieser erweiterten Logik, das noch die volle Ausdrucksstärke hat, aber (wohl im Gegensatz zur vollen Logik) die Hoffnung auf ein brauchbares Entscheidungsverfahren erlaubt.

Horst Reichel: Induktive Definition mit partiellen Konstruktoren / Initiale Einschränkungen / Coalgebren Im ersten Teil des Vortrags wurden algebraische Spezifikationen parametrischer abstrakter Datentypen (PADT’s) mit partiellen Konstruktoren auf der Basis gleichungspartieller algebraischer Theorien und deren Ausdrucksstärke hinsichtlich partiell-rekursiver Funktionen diskutiert. Im zweiten Teil wurde die initiale Semantik der Spezifikation von PADT’s zur Verhaltenssemantik erweitert, um den Anforderungen des Implementationsbegriffes gerecht zu werden. Abschließend wurden als eine Alternative zur Verhaltenssemantik terminale Coalgebren eingeführt und die Coinduktion als allgemeine Methode zur Manipulation von endlichen und unendlichen Verhaltensmustern vorgestellt.

Heiko Vogler: Funktional–logische Programmierung / Baumübersetzer / Attributgrammatiken und Logikprogramme Im ersten Teil des Vortrags wurde eine Einführung in die funktional–logische Programmierung gegeben und dabei genauer auf das bei ihrer Implementierung auftretende Problem der E– Unifikation eingegangen. Im zweiten Teil des Vortrags untersuchte Herr Vogler an Hand von top–down–Baumübersetzern einige in der Theorie der Baumübersetzer relevante Fragestellungen. Insbesondere wurde ein Inklusionsdiagramm für verschiedene Teilklassen von top–down– Baumübersetzungen angegeben. Der letzte Teil des Vortrags diente der Diskussion des Zusammenhangs zwischen Attributgrammatiken und sogenannten orientierbaren Logikprogrammen.

Steffen Hölldobler: Resolution und Unifikation / Fluent–Kalkül Zunächst wurden die für die Logikprogrammierung fundamentalen Begriffe der Resolution und der Unifikation erläutert. Weiterhin verdeutlichte Herr Hölldobler den notwendigen Übergang von der Unifikation zur E–Unifikation, falls zu den Logikprogrammen Gleichungen hinzugenommen werden. Mit vier typischen Problemen aus der Wissensrepräsentation wurde der Übergang zu ressourcenorientierten Systemen motiviert, von denen der Fluent–Kalkül näher vorgestellt wurde. Dieser beruht im wesentlichen auf der Verwendung einer Gleichungstheorie, die durch Kommutativität, Assoziativität und durch die Existenz eines neutralen Elementes induziert wird.

Karsten Schmidt: Symmetrien in Petrinetzen / Analyse algebraischer Petrinetze In diesen beiden Vorträgen wurden Analyseverfahren für Petrinetze vorgestellt. Im ersten Teil ging es um die Berechnung von Netzsymmetrien, deren Kenntnis für die Reduzierung des Aufwandes anderer Analyseverfahren nützlich ist. Im zweiten Teil wurde der symbolische Invariantenkalkül für algebraische High–Level–Netze präsentiert. Dort werden Techniken aus der Theorie abstrakter Datentypen, z.B. Termersetzung oder E–Unifikation, eingesetzt, um Invarianten algebraischer Netze zu verifizieren, Erzeugendensysteme zu berechnen oder den Anwender bei der interaktiven Suche nach Invarianten maschinell zu unterstützen.

Sven–Erik Bornscheuer: Parakonsistente Modellierung gleichzeitiger Aktionen Motiviert durch die Notwendigkeit einer nachvollziehbaren Semantik für formale Spezifikationen dynamischer Systeme, wurde (beispielhaft) die Sprache A_{C}^{+} aus der Familie der sogenannten Action Description Languages eingeführt. Sie erlaubt die parakonsistente Modellierung gleichzeitiger Aktionen und wurde, wie andere Mitglieder dieser Sprachfamilie, korrekt und vollständig in eine entsprechende Variante des Fluent–Kalküls übersetzt. Die Verwendung solcher Sprachen zum Vergleich verschiedener Formalismen (via Übersetzung) scheint gerade auch im Rahmen des Graduiertenkollegs sinnvoll.

Helko Lehmann: Aktionen, Bedingungen, Ressourcen Es wurden einige Probleme bei der Integration von ressourcenorientierten und eigenschaftsorientierten Ansätzen zur Beschreibung diskreter dynamischer Systeme dargestellt. Eine beide Ansätze vereinigende Aktionsbeschreibungssprache wurde präsentiert, in der auch die Effekte nebenläufiger Prozesse spezifiziert werden können. Es wurde auf eine Variante des Fluentkalküls hingewiesen, die die Ableitung logischer Aussagen über in der Aktionsbeschreibungssprache spezifizierten Systemen gestattet.

Markus Lohrey: Ressourcenbasierte Modelle In diesem Vortrag wurden drei Formalismen zur Beschreibung ressourcenbasierter Systeme beschrieben, nämlich der konjunktive Planungskalkül, die algebraischen Petrinetze und die lineare Logik. An Hand eines Beispiels wurde die Äquivalenz dieser drei Formalismen verdeutlicht. Daneben gab Herr Lohrey einen Einblick in die von Meseguer eingeführte Rewrite Logic. Der Vortrag wurde mit einer Übersicht über die für ressourcenbasierte Systeme und deren Zusammenhänge relevante Literatur beendet.

Christian Urban: Normalisierung und Cut–Eliminierung Dieser Vortrag motivierte als erstes die ”Beweise–als–Programme“–Sichtweise für intuitionistische Logik. Danach wurden die Schwierigkeiten der Cut–Eliminierung bei klassischen Beweisen herausgearbeitet und Girards lineare Logik eingeführt, welche sich bei der Cut–Eliminierung besser verhält. An Beispielen wurde gezeigt, wie lineare Beweise als Berechnungen in Transitions– und Planungssystemen aufgefaßt werden können.

Veranstaltungen, die für das Gradiertenkolleg im Sommersemester 97 und im Wintersemester 97/98 relevant sind

Im Rahmen des Graduiertenkollegs finden jeweils dienstags in der Zeit von 13.15 Uhr bis 16.30 Uhr Vorlesungen und Vorträge statt. Sechs Vorträge werden von Gastdozenten gehalten. Weitere sieben bis acht Vorträge realisieren die Stipendiaten. Vorlesungen innerhalb des Kollegs im Sommersemester 1997:

1.- 6. Woche: Universelle Algebra (Prof. Pöschel)
7.-12. Woche: Tree Transducer (Prof. Vogler)

Vorlesungen innerhalb des Graduiertenkollegs im Wintersemester 1997/98:

1.- 6. Woche: Kategorien (Prof. Reichel)
7.-12. Woche: Horn-Klauseln (Prof. Hölldobler)

Termine:

08.04.97:  Erste Vorlesung zur Universellen Algebra
11.04.97, 13.00 Uhr: Feierliche Eröffnung des Graduiertenkollegs

u. a. mit einem Vortrag von Prof. Manfred Broy

Einige Lehrveranstaltungen im Sommersemester 1997 Vorlesungen:

Prof. Droste:  Algebraische Grundlagen der Informatik,

Vorl.: Mi/Do 6./7.DS, WIL C 129, Übung: Di 3.DS, WIL C 102

Prof. Hölldobler: Wissensverarbeitung

Vorl.: Mi 5./6.DS, GRU 454, Übung: Do 5.DS, GRU 454

Prof. Reichel:  Spezifikation und Verifikation

Vorl.: Mi 3.DS, GRU 358, Übung: Di 3.DS, GRU 358

Dr. Seidel:  Kategorien Theorie,

Vorl.: Fr 5.DS, WIL A 120

Prof. Vogler:  Formale Modelle zur syntaxgesteuerten Übersetzung

Vorl.: Mi 5.DS, GRU 150, Übung: Do 6.DS, GRU 353

Hauptseminare:

Prof. Hölldobler: Intellektik, Do 6.DS, GRU 454
Prof. Reichel:  Semantik reaktiver Systeme, Mi 4.DS, GRU 359
Prof. Vogler:  Spezifikation diskreter Prozesse, Di 4./5.DS, GRU 150

Proseminar:

Prof. Reichel:  Grundlagen der Rekursion, Di 2.DS, GRU 358

Seminar innerhalb des Graduiertenkollegs im Wintersemester 1997/98 Durchführung eines Seminars zu einem Buch über Formalismen zur Spezifikation und Programmierung einer Dampferzeugersteuerung [ABL96]. Alle Texte und Programme des Buches sind auf einer CD-ROM enthalten.

Literatur

[ABL96] J.R. Abrial, E. Börger, and H. Langmaack, editors. Formal methods for industrial applications: specifying and programming the steam boiler control, volume 1165 of Lecture Notes in Computer Science. Springer-Verlag Inc., New York, NY, USA, 1996. (with CD-ROM).