Seminar zur Theorie paralleler Prozesse, WS 97/98

Prozeßkalküle und Model Checking

Zuordnung: theoretisch

Die Termine

Die Themen:

On the fly model checking for LTL

Es wird ein Tableaux-Verfahren vorgestellt, welches on-the-fly-model-checking für die Logik LTL ermöglicht.
Literatur: [GPVW95] Betreuer: Thomas Noll

Model checking for CTL using automata

Hier werden automatentheoretische Ansätze zur Behandlung des Model checking-Problems für CTL vorgestellt.
Literatur: [VBW94, Eme96] Betreuer: Thomas Noll

Model checking the -calculus using the tableaux method

Die Grundidee besteht darin, einen Graphen zu konstruieren, der die Modelle der gegebenen Formel repräsentiert. Eigenschaften dieses Graphen lassen dann Rückschlüsse auf die Erfüllbarkeit der Formel zu.
Literatur: [SW91, Eme96, Sti96b] Betreuer: Thomas Noll

Model checking für den -Kalkül und Alternierungstiefe

Hier soll untersucht werden, welchen Einfluß die Alternierungstiefe einer Formel, also die Anzahl der Wechsel zwischen (geschachtelten) kleinsten und größten Fixpunkten, auf die Ausdrucksstärke der Logik und die Komplexität des Model checking-Problems hat.
Literatur: [EL86, Eme97] Betreuer: Thomas Noll

Bisimulation und Games

Es wird gezeigt, daß die Entscheidbarkeit der Bisimulation als Ehrenfeucht-Fraissé-Spiel aufgefaßt werden kann. Hierbei sind zwei Prozesse genau dann bisimilar, wenn der zweite Spieler eine Gewinnstrategie hat.
Literatur: [Sti96a] Betreuer: Martin Leucker

Model checking und Games

Es wird gezeigt, daß Model checking als ein Ehrenfeucht-Fraissé-Spiel aufgefaßt werden kann, für welches der zweite Spiele eine Gewinnstrategie besitzt genau dann wenn das gegebene Modell die zu untersuchende Formel erfüllt.
Literatur: [Sti95, Sti96a] Betreuer: Martin Leucker

Basic Process Algebra

In BPA wird das aus CCS bekannte Prefixing durch das Komplexprodukt von Prozeßausdrücken ersetzt. Hierdurch werden infinite-State Transitionssysteme beschrieben, welche kontextfreie Eigenschaften haben. Neben dem Kalkül BPA werden Contextfree-Processes vorgestellt und deren Äquivalenz zu BPA-Prozessen gezeigt. Außerdem wird eine Logik eingeführt, deren Ausdrucksstärke den BPA-Prozessen entspricht.
Literatur: [HM96, FGP93] Betreuer: Frank Huch

Basic Parallel Processes

Im Gegensatz zu BPA wird hier die kontextfreie Eigenschaft des Parallel-Operators aus CCS untersucht. Außerdem werden Concurrent-Contextfree-Processes vorgestellt und gezeigt, daß diese äquivalent zu BPP-Prozessen sind.
Literatur: [HM96] Betreuer: Frank Huch

Model checking für kontextfreie Prozesse

Es wird ein Model checking Algorithmus für kontextfreie Prozesse vorgestellt.
Literatur: Burkart92 Betreuer: Frank Huch

Traces

Bei Traces wird im Gegensatz zu allgemeinen Transitionssystemen die Reihenfolge nicht-abhängigen Aktionen nicht unterschieden. Dieser Ansatz von Mazurkiewicz führt auf die algebraische Theorie der partiell kommutativen Monoide. Es werden die grundlegenen Ideen dieser Theorie vorgestellt und auf besondere Aspekte in Zusammenhang mit Logiken für Traces eingegangen.
Literatur: [DM96] Betreuer: Martin Leucker

Model checking für Traces

Traces stellen ein etwas abstrakteres (im obigen Sinne) semantisches Modell zur Beschreibung von Nebenläufigkeit dar. Es wird ein Automatenmodell vorgestellt, welches dem Begriff der Traces entspricht und für Model checking verwendet werden kann.
Literatur: [PP95] Betreuer: Martin Leucker

Programmlogiken

Programmlogiken dienen zur Analyse und Verifikation sequentieller Programme. Es wird die propositionale Programmlogik PDL vorgestellt und ein Vergleich zu den in der Vorlesung ,,Theorie paralleler Prozesse`` definierten Logiken durchgeführt.
Literatur: [KT90] Betreuer: Frank Huch