Analyse von Petrinetzmodellen (SE)
Prof. Dr. Matthias Weidlich
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 | Fr 9-11 |
| Raum | RUD 25, 3.101 |
| Agnes | 3313099 |
| Studiengang | Monobachelor Informatik |
| Empfohlene Vorkenntnisse |
Module "Modellierung und Spezifikation" oder "Software Engineering" |
| Einführung |
Terminplanung
| Datum | Themen/Vortragende |
|---|---|
| 20.04.2018 | Intro |
| 27.04.2018 | entfällt |
| 04.05.2018 | entfällt |
| 11.05.2018 | 1 (Mitev), 5 (Liepe) |
| 18.05.2018 | 6 (Atanasov) |
| 25.05.2018 | 11 (Antipov), 15 (Vu) |
| 01.06.2018 | 12 (Behrent), 17 (Peters) |
| 08.06.2018 | 19 (Schulze), 14 (Vandamme) |
| 15.06.2018 | 22 (Petersen), 23 (Enseleit) |
| 22.06.2018 | |
| 29.06.2018 | |
| 06.07.2018 | |
| 13.07.2018 | |
| 20.07.2018 |
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 | Dragomir Mitev |
| 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 | |
| 3 | Der Überdeckbarkeitsgraph | Starke: "Analyse von Petri-Netz-Modellen", Kap. 5, und Schmidt: "Model-Checking with Coverability Graphs" | |
| 4 | Platz- und Transitionsinvarianten | Starke: "Analyse von Petri-Netz-Modellen", Kap. 11 | |
| 5 | Verteilte Abläufe | Reisig: "Petrinetze", Kap. 4.4 und 4.7 | Jonas Liepe |
| 6 | Regionentheorie | Desel, Reisig: "The Synthesis Problem of Petri Nets." und Cortadella et al: "Deriving Petri Nets from Finite Transition Systems" | Aleksandar Atanasov |
| 7 | Symmetrien | Karsten Schmidt: "How to calculate symmetries of Petri nets" | |
| 8 | Partial Order Reduction / Stubborn Sets | Antti Valmari: "The State Explosion Problem", Kap. 7.4 | |
| 9 | Unfoldings | McMillan: "Symbolic Model Checking", Kap. 6, und Esparza et al: "Model Checking Using Net Unfoldings" | |
| 10 | Beweisgraphen | Reisig: "Elements of distributed Algorithms", Kap. VIII | |
| 11 | High-Level-Petrinetze | Reisig: "Petri Nets and Algebraic Specifications.", Reisig: "Petrinetze" und Reisig: "Elements of distributed Algorithms", Kap. III | Leonid Antipov |
| 12 | Zeit und Petrinetze | Starke: "Analyse von Petri-Netz-Modellen", Kap. 17,18,19 | Annalyn Behrent |
| 13 | Stochastische Petrinetze | Falko Bause und Pieter S Kritzinger "Stochastic Petri Nets - An Introduction to the Theory" | |
| 14 | Workflow-Netze | W.M.P. van der Aalst: "Verification of Workflow Nets" | Marcel Vandamme |
| 15 | High-level Invarianten | Reisig: "Petrinetze - Modellierungstechnik, Analysemethoden, Fallstudien" Kap. 13 | Duc Anh Vu |
| 16 | CPN-Tools | http://cpntools.org | |
| 17 | Vergleich von Werkzeugen für die Modellierung und Analyse | http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/ | Aljoscha Peters |
| 18 | Die Sweep-Line-Methode für Petrinetze | Karsten Schmidt: "Automated generation of a progress measure for the sweep-line method" | |
| 19 | Analyse von BPMN-Modellen |
Remco M. Dijkman , Marlon Dumas , Chun Ouyang: "Formal Semantics and Analysis of BPMN Process Models using Petri Nets"
|
Martin Schulze |
| 20 | Komposition von Petrinetzen | Reisig: "Simple Composition of Nets" | |
| 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" | |
| 22 | Petrinetze und formale Sprachen |
Matthias Jantzen: "Language theory of Petri nets"
|
Lucas Archimedes Gregório Petersen |
| 23 | Stabile Ungleichungen in Petrinetzen |
M. Triebel, J. Sürmeli: "Characterizing Stable Inequalities of Petri Nets"
|
Ronja Iris Enseleit |
| 24 | Verfeinerung in Petrinetzen |
W. Brauer, R. Gold, W. Vogler: "A survey of behaviour and equivalence preserving refinements of petri nets"
|