Blockseminar: 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.
Zum Seminar
| Zuordnung | Hauptstudium, Theoretische Informatik | |
|---|---|---|
| Einführungsveranstaltung | Montag, 27.10.2008, 17 Uhr (s.t.), Raum IV.410 | |
| Ort & Zeit | Blockseminar, Januar 2009 (siehe unten) | |
| Dozent | Peter Massuthe | |
| Studienpunkte | 3 |
Termine
Die Einführungsveranstaltung findet am Montag, den 27.10.2008, um 17:00 Uhr statt (Raum IV.410). Wer nicht an der Einführungsveranstaltung teilnehmen kann, muss sich per email abmelden - sonst werden die Themen an andere Anwesende vergeben!
Das Blockseminar findet dann an 3 Terminen im Januar 2009 statt:
- Freitag, den 9.1.2009, in Raum 1.303 in RUD 26 (!),
- Samstag, den 10.1.2009, in Raum III.113 in RUD 25, sowie
- Samstag, den 17.1.2009, in Raum III.113 in RUD 25,
jeweils von 9:00 bis 17:00 Uhr.
Voraussetzung für einen Seminarschein ist die Teilnahme an allen drei Terminen im Januar!
Vorträge
Jeder Teilnehmer hält einen 60-minütigen Vortrag, anschließend haben wir Zeit für 15 Minuten Diskussion. Damit schaffen wir 5 Vorträge pro Tag nach folgendem Schema:
| Zeit | ||
|---|---|---|
| 09:00 - 10:15 Uhr | Vortrag | |
| 10:15 - 11:30 Uhr | Vortrag | |
| 11:30 - 13:00 Uhr | Mittagspause | |
| 13:00 - 14:15 Uhr | Vortrag | |
| 14:15 - 15:30 Uhr | Vortrag | |
| 15:30 - 15:45 Uhr | Pause | |
| 15:45 - 17:00 Uhr | Vortrag |
Themen und Literatur
Eine Liste, wer welches Thema bearbeitet, gibt es hier: 
.
| Thema | Literatur |
|---|---|
| 1) "Spezielle Netzklassen" | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 3 und 4.1 |
| 2) "Deadlocks und Fallen" | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 4.2 und 4.3 |
| 3) "Überdeckbarkeitsgraph" | Starke: "Analyse von Petri-Netz-Modellen", Kap. 5, und Schmidt: "Model-Checking with Coverability Graphs" |
| 4) "Strukturelle Reduktion" | Girault,Valk: "Petri Nets for Systems Engineering", Kap. 15.1, Starke: "Analyse von Petri-Netz-Modellen", Kap. 9, und v. d. Werf: "Analysis of well-formedness and soundness by reduction techniques and their implementation" |
| 5) "Regionentheorie" | Desel, Reisig: "The Synthesis Problem of Petri Nets." und Cortadella et al: "Deriving Petri Nets from Finite Transition Systems" |
| 6) "Invarianten" | Starke: "Analyse von Petri-Netz-Modellen", Kap. 11 |
| 7) "Fairness" | Völzer: "Fairness, Randomisierung und Konspiration in verteilten Algorithmen", Kap. 3-6 |
| 8) "Kompositionale Verifikation" | Juan: "Compositional Verification of Concurrent Systems Using Petri-Net-Based Condensation Rules" |
| 9) "Symmetriereduktion" | Schmidt: "How to calculate symmetries of Petri nets" |
| 10) "Partial Order Reduction" | Antti Valmari: "The State Explosion Problem", Kap. 7.4 |
| 11) "Unfoldings" | McMillan: "Symbolic Model Checking", Kap. 6, und Esparza et al: "Model Checking Using Net Unfoldings" |
| 12) "Beweisgraphen" | Reisig: "Elements of distributed Algorithms", Kap. VIII |
| 13) "Zeitpetrinetze" | Starke: "A Memo on Time Constraints in Petri Nets" |
| 14) "High-Level Petrinetze" | Reisig: "Petri Nets and Algebraic Specifications." und Reisig: "Elements of distributed Algorithms", Kap. III |
| 15) "High-Level Invarianten" | Reisig: "Petri Nets and Algebraic Specifications." und Smith: "Principles of High-Level Net Theory." |
Vortragsfolien
| Thema | Folien |
|---|---|
| 1) "Spezielle Netzklassen" |
|
| 2) "Deadlocks und Fallen" | ausgefallen |
| 3) "Überdeckbarkeitsgraph" |
|
| 4) "Strukturelle Reduktion" |
|
| 5) "Regionentheorie" |
|
| 6) "Invarianten" |
|
| 7) "Fairness" |
|
| 8) "Kompositionale Verifikation" |
|
| 9) "Symmetriereduktion" | ausgefallen |
| 10) "Partial Order Reduction" |
|
| 11) "Unfoldings" | ausgefallen |
| 12) "Beweisgraphen" |
|
| 13) "Zeitpetrinetze" |
|
| 14) "High-Level Petrinetze" |
|
| 15) "High-Level Invarianten" | ausgefallen |
Theorie der Programmierung | Kontakt | zuletzt geändert am 16.08.2009 13:05