Unendliche Transitionssysteme

» Diese Veranstaltung wird auf deutsch gehalten.

Vorlesung im Sommersemester 2005

ArtTermine/OrtBeginnVeranstalter
V2 Mi 10:00 - 11:30 AH VI 13.04.2005 Löding
Ü1 Mi 15:00 - 15:45 AH VI 20.04.2005 Löding, Altenbernd

Inhalt

Automatenmodelle mit unendlichem Speicher (z.B. Kellerautomaten, kommunizierende Automaten oder Petri-Netze) können zur Modellierung vieler in der Praxis auftretender Systeme, etwa mit Laufzeitstack, Kommunikationspuffern oder verteilter Architektur, verwendet werden.

Der Transitionsgraph eines solchen Automaten hat als Knoten die Konfigurationen des Automaten und als Kanten die entsprechenden Transitionen. Da der verwendete Speicher prinzipiell unbeschränkt ist, sind die entstehenden Transitionsgraphen unendlich.

In dieser Vorlesung werden Entscheidungsprobleme für solche unendlichen Transitionsgraphen behandelt, die in Anwendungen, etwa in der Verifikation, eine zentrale Rolle spielen. Der Schwerpunkt liegt dabei auf Erreichbarkeitsproblemen, also Fragen der Form: "Gegeben ein Transitionsgraph und zwei Konfigurationen, ist die eine von der anderen aus erreichbar?"

Der Inhalt der Vorlesung entspricht in großen Teilen den Kapiteln 4-6 der Vorlesung Applied Automata Theory aus dem Sommersemester 2004.

Kombination mit anderen Veranstaltungen

Diese Vorlesung kann mit der Vorlesung Advanced Theory of Finite Automata zu einer vierstündigen Vorlesung (V4, Ü2) kombiniert werden. In dieser Kombination entspricht der Stoff in etwa dem Inhalt der Vorlesung Applied Automata Theory aus dem Sommersemester 2004.

Wichtiger Hinweis: Die beiden Vorlesungen werden separat behandelt. Die Kriterien für die Ausgabe von Übungsscheinen sind unabhängig für beide Vorlesungen. Bei Erfüllung der Kriterien werden kleine Übungsscheine (V2, Ü1) ausgegeben. Wer beide kleinen Übungsscheine erhalten hat, kann diese gegen einen großen Übungsschein (V4, Ü2) eintauschen.

Notwendige Vorkenntnisse

Diese Vorlesung wendet sich an Studierende ab dem 5. Fachsemester. Kenntnisse aus der Grundstudiumsvorlesung Automatentheorie und formale Sprachen werden vorausgesetzt.

Prüfungsleistung

Um einen Übungsschein (V2, Ü1) zu bekommen, müssen die beiden folgenden Bedingungen erfüllt werden:

  1. Es müssen 50% der Punkte in den Übungen erreicht werden. Es zählen nur die Aufgaben zu der Vorlesung Unendliche Transitionssysteme, nicht die Aufgaben der anderen Vorlesung.
  2. Die Abschlussklausur muss bestanden werden.

Wer genügend Punkte in den Übungen erreicht hat, aber die Abschlussklausur nicht mitgeschrieben oder nicht bestanden hat, ist zur Teilnahme an einer Nachprüfung berechtigt.

Wer nicht genügend Punkte in den Übungen erreicht hat, kann die Abschlussklausur mitschreiben, erhält aber auch bei Bestehen der Klausur keinen Übungsschein.

Abschlussklausur

Die Abschlussklausur wird am Montag, 25.7.2005 um 17.00 Uhr im Hörsaal Aula 2 geschrieben.

Credit Points

4 ECTS