Seminar: Analyse von Petrinetz-Modellen

Petrinetze werden zur Modellierung verteilter Systeme verwendet. Zustandsänderungen in einem Petrinetz-Modell werden verstanden als Erzeugen und Vernichten von Ressourcen (statt des sonst üblichen Lesens und Schreibens von Variablen). Dadurch ergeben sich interessante algorithmische Analysemöglichkeiten, die in diesem Seminar vorgestellt werden.

Zur Prüfung

Wer im Sommersemester 2007 die Vorlesung "Algebraische Spezifikation von Software und Hardware" belegt hat, kann sie mit diesem Seminar zu einem Halbkurs kombinieren.

Informationen zur Kombinationsprüfung "Algebraische Spezifikation von Software und Hardware" / "Analyse von Petrinetz-Modellen" sind hier nachzulesen:

Zuordnung	Hauptstudium, Praktische Informatik
Zeit	Dienstag, 11.3.2008, ab 09:00 Uhr
Ort	RUD 25, Raum IV.410
Prüfer	Prof. Schlingloff / Peter Massuthe
Prüfungsart	Mündliche Einzelprüfung

Anmeldung ab sofort bis 26.2.2008 bei Frau Heene, Raum IV.417.

Prüfungsrelevante Themen

Für den Teil "Analyse von Petrinetz-Modellen" sind folgende Themengebiete relevant. Die jeweils aufgezählten Unterpunkte sollen als Schwerpunkt im jeweiligen Gebiet gesehen werden. Literaturhinweise zum Nachlesen sind weiter unten angegeben, die jeweiligen Foliensätze sollen das Verständnis der Paper unterstützen.

0) Grundlagen von Petrinetzen

• Petrinetz, Lebendigkeit, Sicherheit, Beschränktheit, Erreichbarkeit, Erreichbarkeitsgraph, ...

1) Spezielle Netzklassen

• Synchronisationsgraph, Zustandsmaschine, Free-Choice-Netz, Extended FC-Netz, Extended-Simple-Netz
• Zusammenhang zwischen Netzklassen und Fragestellungen der Analyse

2) (Strukturelle) Deadlocks, Fallen

• Definitionen, Eigenschaften von Deadlocks und Fallen
• Analyse mittels Deadlock-Falle-Eigenschaft

3) Invarianten

• Definition, Berechnung, Nachweis von (Low-Level-)Invarianten
• Analyse mit Invarianten

4) Regionentheorie

• Begriffe Region, redundante / minimale Region, elementares Transitionssystem, ...
• Synthese eines Netzes aus einem Transitionssystem

5) Überdeckbarkeitsgraph

• Definition und Eigenschaften
• Konstruktion

6) Partial Order Reduction

• (Statisch) sture Mengen, stur reduzierter Erreichbarkeitsgraph
• Konstruktion eines stur reduzierten Erreichbarkeitsgraphen

7) Unfoldings

• Begriffe und Eigenschaften
• Konstruktion von Unfoldings

8) Beweisgraphen

• Begriffe, Eigenschaften von Beweisgraphen
• Nachweis von Eigenschaften mittels Beweisgraphen

9) Zeitnetze

• Varianten von Zeitnetzen, verschiedene Schaltstrategien
• Verhältnis untereinander und zum unterliegenden Petrinetz

10) High-Level-Petrinetze

• Definitionen (Signatur, Struktur, Term, Modus, ...)
• High-Level-Petrinetze vs. Petrinetz-Schemata
• Zusammenhang mit Low-Level-Petrinetzen

11) High-Level-Invarianten

• Definition, Nachweis
• Bezug zu Low-Level-Petrinetzen

Zum Seminar

Zuordnung	Hauptstudium, Theoretische Informatik
Zeit	Mo 11-13 Uhr
Ort	RUD 25, III. 113
Dozent	Peter Massuthe

Termine

Termin	Tag	Thema 1	Thema 2
0.	29.10.2007	Einführung und Themenvergabe
1.	06.11.2007	"Spezielle Netzklassen" I
2.	12.11.2007	"Deadlocks und Fallen" I	"Partial Order Reduction" I
3.	19.11.2007	"Spezielle Netzklassen" II
4.	26.11.2007	"Überdeckbarkeitsgraph" I	"Deadlocks und Fallen" II
5.	03.12.2007	"Regionentheorie" I	"Partial Order Reduction" II
6.	10.12.2007	"Beweisgraphen" I	"Überdeckbarkeitsgraph" II
7.	17.12.2007	"Unfoldings" I	"Regionentheorie" II
8.	07.01.2007	"High-Level Petrinetze" I
9.	14.01.2008	"Zeitpetrinetze" I	"Unfoldings" II
10.	21.01.2008	"High-Level Petrinetze" II
11.	28.01.2008	"High-Level Invarianten" I
12.	04.02.2008	"Beweisgraphen" II	"Zeitpetrinetze" II
13.	11.02.2008	"High-Level Invarianten" II

Zuordnung und Literatur

Thema	Vortragender	Literatur
Einführung und Themenvergabe	Peter Massuthe	Desel, Reisig: "Place/Transition Petri Nets"
"Spezielle Netzklassen"	Leonard Kern	Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 3 und 4.1
"Deadlocks und Fallen"	Steve Reich	Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 4.2 und 4.3
"Überdeckbarkeitsgraph"	Martin Filip	Starke: "Analyse von Petri-Netz-Modellen", Kap. 5, und Schmidt: "Model-Checking with Coverability Graphs"
"Invarianten"		Starke: "Analyse von Petri-Netz-Modellen", Kap. 11
"Regionentheorie"	Rico Bergmann	Desel, Reisig: "The Synthesis Problem of Petri Nets." und Cortadella et al: "Deriving Petri Nets from Finite Transition Systems"
"Partial Order Reduction"	Janine Ott	Antti Valmari: "The State Explosion Problem", Kap. 7.4
"Unfoldings"	Yves Radunz	McMillan: "Symbolic Model Checking", Kap. 6, und Esparza et al: "Model Checking Using Net Unfoldings"
"Beweisgraphen"	Mike Herzog	Reisig: "Elements of distributed Algorithms", Kap. VIII
"High-Level Petrinetze"	Jan Suermeli	Reisig: "Petri Nets and Algebraic Specifications." und Reisig: "Elements of distributed Algorithms", Kap. III
"Zeitpetrinetze"	Hartmut Lackner	Starke: "A Memo on Time Constraints in Petri Nets"
"High-Level Invarianten"	Johannes Fichte	Reisig: "Petri Nets and Algebraic Specifications." und Smith: "Principles of High-Level Net Theory."

Foliensätze zu den Themen

Thema	Folien 1	Folien 2
"Spezielle Netzklassen"
"Deadlocks und Fallen"
"Invarianten"	-	-
"Regionentheorie"
"Überdeckbarkeitsgraph"
"Partial Order Reduction"
"Unfoldings"
"Beweisgraphen"
"Zeitpetrinetze"
"High-Level Petrinetze"
"High-Level Invarianten"