Kommunikation und parallele Prozesse

Die Theorie der kommunizierenden nebenläufigen Agenten gehört zum Kern der theoretischen Informatik. Das Ziel dies Kurses ist es, ein formalisiertes Fundament des Begriffs “Prozess” zu entwickeln, der sich hinter jedem modernen Software- oder Hardware-System versteckt, von einem Arbeitszyklus eines Warenautomaten bis zu den Kernprozessen hinter der UNIX-Konsole.

In diesem Kurs stellen wir die Grundlagen dieser Theorie bereit, mit Milner’s Kalkül der //Concurrent Communicating Systems// (CCS) als Ausgangspunkt. Im Gegensatz zu ihrem engen Verwandten, der Automatentheorie, ist die Theorie der kommunizierenden Prozesse auf das reaktive Verhalten von Systemen ausgerichtet statt auf formale Sprachen. In CCS führt dies zu einer Präsentation von Agenten als verzweigte Strukturen; diese werden rekursiv über einen syntaktischen Formalismus, eine Prozessalgebra, erzeugt, ähnlich wie reguläre Sprachen durch reguläre Ausdrücke beschrieben werden. Das sich daraus ergebende Rahmenwerk hat folgende Bestandteile:

• Eine Pseudo-Programmiersprache mit nebenläufigen Primitiven;
• grundlegende Prinzipien und Techniken für das Schlussfolgern über Prozesse;
• ein sehr einfaches Paradigma synchroner Handshakes durch Lesen/Schreiben von Messages über einen Kanal.

Basierend auf dem elementaren Fall des CCS-Kalküls diskutieren wir

• Formalisierungen anwendungsnaher Beispiele
• Äquivalenzen der formalisierten Multi-Agenten-Systeme mithilfe des grundlegenden Begriffs der Bisimulation
• formale Verifikation von Prozesseigenschaften.

Wir fahren fort, indem wir den pi-Kalkül definieren, der CCS durch dynamische Erzeugung und Kommunikation von Kanalnamen erweitert, so dass die Kommunikationsstruktur von Prozessen dynamisch rekonfiguriertbar wird.

Schließlich betrachten wir verschiedene Systeme der Modallogik zur Spezifikation von Prozessen, wie z.B. Linear temporal Logic, Computational tree logic und der modale µ-Kalkül. Wir untersuchen anhand zahlreicher Beispiele, wie Prozessalgebren in Verbindung mit Prozesslogiken in der Formalen Verifikation benutzt werden können.