Halbordnungssemantik von Petrinetzen

Inhalt der Lehrveranstaltung:

Petrinetze gehören zu den bekanntesten Formalismen zur Modellierung nebenläufiger Systeme und der Analyse deren Verhaltens in vielen Anwendungsfeldern, wie z.B. Kommunikations-Netzwerken, Produktionsanlagen, Geschäftsprozessen oder Webdiensten. Hierbei spielen insbesondere Methoden zur Verhaltens-Simulation und -Verifikation, sowie zur Modellsynthese aus Verhaltensbeschreibungen eine große Rolle.

Das Verhalten von Petrinetzen wird durch Abläufe beschrieben. In dieser Vorlesung soll ein Ablauf durch eine halbgeordnete Ereignismenge gegeben sein. Solche Abläufe erlauben, im Gegensatz zu anderen Ablauf-Semantiken, eine explizite Darstellung von kausaler Unabhängigkeit von Ereignissen. Während derartige halbgeordnete Abläufe in der Theorie seit längerer Zeit betrachtet werden, finden sie in jüngerer Zeit auch in Anwendungen Beachtung. Diese Entwicklung wird begleitet von einer Reihe neuer theoretischer Erkenntnisse, welche sich in neuartigen und effizienteren Simulations-, Verifikations- und Synthesemethoden niederschlagen.

In der Vorlesung wird die traditionelle Theorie der Halbordnungssemantik bis hin zu aktuellsten Forschungsergebnissen präsentiert, einschließlich von Resultaten des von der Deutschen Forschungsgemeinschaft (DFG) geförderten Projekts "Synthese von Petrinetzen aus Szenarien" ( SYNOPS). Begleitend wird mit Hilfe des Software-Werkzeugs Viptool (und anderen Werkzeugen) die Anwendung der theoretischen Erkenntnisse geübt.

Aus dem Inhalt:

• Partielle Ordnungen
• Prozess-Netze
• Halbgeordnete Abläufe
• Markenflüsse
• Effiziente Verifikation halbgeordneter Abläufe
• Prozess-Terme
• vollständige Prozesssemantiken
• Entfaltungen
• Synthese aus Halbordnungen
• Erweiterte Netzklassen und kausale Strukturen

Diese Vorlesung bildet die Grundlage eines Seminars zu Inhalten des Projekts SYNOPS, welches sich zur Vorbereitung auf eine Diplomarbeit eignet.

 

Vorkenntnis für die Lehrveranstaltung:

Grundkenntnisse in der Syntax und der sequentiellen Semantik von Petrinetzen sind wünschenswert, aber nicht zwingend erforderlich.

Literatur zur Lehrveranstaltung:

• E. Best, R. R. Devillers: Sequential and Concurrent Behaviour in Petri Net Theory. Theor. Comput. Sci. 55(1), 1987, 87-136.
• W. Vogler: Modular Construction of Partial Order Semantics of Petri Nets. LNCS 625, 1992.
• W. Reisig, G. Rozenberg (Hrsg.): Lectures on Petri Nets I: Basic Models. LNCS 1491, 1998.
• J. Esparza, S. Römer, W. Vogler: An Improvement of McMillan's Unfolding Algorithm. LNCS 1055, 1996, 87-106.
• G. Juhas: Are these events independent? It depends!. Habilitationsschrift, Eichstätt, 2005.
• Projekt-Homepage VipTool:
• Projekt-Homepage SYNOPS

Übungen

Zur Vertiefung des Vorlesungsstoffs wird die Vorlesung durch eine Übung ergänzt. Es werden wöchentlich Übungsblätter mit Übungsaufgaben herausgegeben. Die Übungsblätter sollen von Woche zu Woche bearbeitet werden. In der Übung werden die Lösungen der Übungsaufgaben besprochen. Lösungsvorschläge werden nicht abgegeben und nicht korrigiert. Stattdessen ist zweimaliges Vorrechnen obligatorisch.

Übungsgruppen

Am Donnerstag, den 23.4., ist Vorbesprechung von 12.15 bis 13.45 im Raum 1007 L.

Übungsblätter

• Wöchentlich wird online ein Übungsblatt herausgegeben; Wochentag steht noch nicht fest; Start in der zweiten Veranstaltungswoche ab 27.4.
• Bearbeitungszeit: bis zum Übungstermin in der nächsten Woche
• Besprechung der Lösungen in den Übungsgruppen. Lösungen werden nicht abgegeben und korrigiert!
• In den Übungen ist für jeden Studenten zweimal Vorrechnen Pflicht

 

Klausur

• Termine: Klausur in der letzten Vorlesung, also am 21.7.2008 im Raum der Vorlesung..
• Prüfungsmodul: Teilnahmevorausetzung für die Klausur ist
  • die fristgerechte elektronische Anmeldung in LectureReg zur Übungsgruppe (Anmeldezeitraum 20.4. - 30.4.)
  • 10 Punkte aus dem Übungsbetrieb durch Vorrechnen. Zu jedem der zwei Vorlesungsteile muss einmal vorgerechnet werden.
  • die fristgerechte elektronische Anmeldung zur jeweiligen Klausur (Anmeldezeitraum 1.7. - 15.7.)
  • die fristgerechte Anmeldung zum Prüfungsmodul bei STUDIS (Anmeldezeitraum 8.6. - 18.6.2009)
  Die Teilnahmeberechtigung ist beschränkt auf das Sommersemester 2009
• Klausurmodalitäten:
  • Bearbeitungszeit jeweils 90 Minuten
  • Alle Teilnehmer unterschreiben die Teilnehmerliste während den Klausuren
  • Es sind keine Hilfsmittel zugelassen (Disqualifikation)
  • Es ist nicht gestattet, eine Kopie des Lösungsteils anzufertigen (Disqualifikation)
  • Die Aufgaben sind selbständig zu erledigen. Kontaktaufnahme zu anderen Teilnehmern oder deren Unterlagen führen zur Disqualifikation
  • Die Arbeiten disqualifizierter Teilnehmer werden mit 5,0 bewertet und dem Prüfungsausschuss gemeldet
  • Studentenausweis und Personalausweis sind zur Klausur mitzubringen

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung:	ab dem 5. Semester
Fachrichtung Lehrveranstaltung:	Informatik
Nummer der Lehrveranstaltung:	7061
Dauer der Lehrveranstaltung:	2 SWS
Typ der Lehrveranstaltung:	V - Vorlesung
Leistungspunkte:	5 LP für V+Ü
Bereich:	Theoretische Informatik
Prüfung:	Klausur und Hausarbeit
Begleitende Lehrveranstaltung(en):	7062
Semester:	alle WS und SS