Analyse von Petrinetzmodellen (SE)
Dr. Jan Sürmeli
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.
| Zeit | Mo 13-15 |
| Raum | RUD 25, 3.101 |
| Agnes | 3313109 |
| Studiengang | Monobachelor Informatik |
| Empfohlene Vorkenntnisse | Module "Modellierung und Spezifikation" oder "Software Engineering" |
(Vorläufige) Terminplanung
| Datum | Themen/Vortragende |
|---|---|
| 19.10.2015 | Intro/Jan |
| 26.10.2015 | entfällt |
| 02.11.2015 | entfällt |
| 09.11.2015 | 2/Marco, 3/Hauke |
| 16.11.2015 | 4/Marcel, 5/Martin |
| 23.11.2015 | 6/Daniel, 7/Konstantin |
| 30.11.2015 | 8/Andrei, 11/Alex |
| 07.12.2015 | 12/Lukas, 22/Sarah |
Themen und Literatur
| Nr | Thema | Literatur (Einstieg) | Vortragende* |
|---|---|---|---|
| 1 | Spezielle Netzklassen | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 3 und 4.1 | - entfällt - |
| 2 | Strukturelle Deadlocks und Fallen | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 4.2 und 4.3 | Marco |
| 3 | Der Überdeckbarkeitsgraph | Starke: "Analyse von Petri-Netz-Modellen", Kap. 5, und Schmidt: "Model-Checking with Coverability Graphs" | Hauke |
| 4 | Platz- und Transitionsinvarianten | Starke: "Analyse von Petri-Netz-Modellen", Kap. 11 | Marcel |
| 5 | Verteilte Abläufe | Reisig: "Petrinetze", Kap. 4.4 und 4.7 | Martin |
| 6 | Regionentheorie | Desel, Reisig: "The Synthesis Problem of Petri Nets." und Cortadella et al: "Deriving Petri Nets from Finite Transition Systems" | Daniel |
| 7 | Symmetrien | Karsten Schmidt: "How to calculate symmetries of Petri nets" | Konstantin |
| 8 | Partial Order Reduction / Stubborn Sets | Antti Valmari: "The State Explosion Problem", Kap. 7.4 | Andrei |
| 9 | Unfoldings | McMillan: "Symbolic Model Checking", Kap. 6, und Esparza et al: "Model Checking Using Net Unfoldings" | - entfällt - |
| 10 | Beweisgraphen | Reisig: "Elements of distributed Algorithms", Kap. VIII | - entfällt - |
| 11 | High-Level-Petrinetze | Reisig: "Petri Nets and Algebraic Specifications.", Reisig: "Petrinetze" und Reisig: "Elements of distributed Algorithms", Kap. III | Alex |
| 12 | Zeit und Petrinetze | Starke: "A Memo on Time Constraints in Petri Nets" | Lukas |
| 13 | Stochastische Petrinetze | Falko Bause und Pieter S Kritzinger "Stochastic Petri Nets - An Introduction to the Theory" | - entfällt - |
| 14 | Workflow-Netze | W.M.P. van der Aalst: "Verification of Workflow Nets" | - entfällt - |
| 15 | High-level Invarianten | Reisig: "Petrinetze - Modellierungstechnik, Analysemethoden, Fallstudien" Kap. 14 | - entfällt - |
| 16 | CPN-Tools | http://cpntools.org | - entfällt - |
| 17 | Vergleich von Werkzeugen für die Modellierung und Analyse | http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/ | - entfällt - |
| 18 | Die Sweep-Line-Methode für Petrinetze | Karsten Schmidt: "Automated generation of a progress measure for the sweep-line method" | - entfällt - |
| 19 | Analyse von BPMN-Modellen |
Remco M. Dijkman , Marlon Dumas , Chun Ouyang: "Formal Semantics and Analysis of BPMN Process Models using Petri Nets"
|
- entfällt - |
| 20 | Komposition von Petrinetzen | Reisig: "Simple Composition of Nets" | - entfällt - |
| 21 | Szenario-basierte Spezifikation mit Petrinetzen | D. Fahland: "Oclets - scenario-based modeling with Petri nets.", D. Fahland, R. Prüfer: "Data and Abstraction for Scenario-Based Modeling with Petri Nets" | - entfällt - |
| 22 | Petrinetze und formale Sprachen |
Matthias Jantzen: "Language theory of Petri nets"
|
Sarah |
| 23 | Stabile Ungleichungen in Petrinetzen |
M. Triebel, J. Sürmeli: "Characterizing Stable Inequalities of Petri Nets"
|
- entfällt - |
| 24 | Verfeinerung in Petrinetzen |
W. Brauer, R. Gold, W. Vogler: "A survey of behaviour and equivalence preserving refinements of petri nets"
|
- entfällt - |