In dieser Theorievorlesung werden die wichtigsten Begriffsbildungen und Ergebnisse der Automatentheorie vorgestellt, die in den Anwendungen bei der Systemkonstruktion und -analyse benötigt werden. Themenstichworte sind:

• Minimierungsverfahren für Automaten (Zustandsäquivalenz, Bisimulation)
• Logiken zur Verhaltensbeschreibung von Automaten (z.B. temporale Logik)
• Baumautomaten und die Auswertung von XML-Dokumenten
• Pushdown-Systeme
• Kommunizierende endliche Automaten, Message-Sequence-Charts
• Hierarchische Systeme
• Petrinetze

Ein Schwerpunkt der Vorlesung wird die Behandlung algorithmischer Fragen über das Verhalten von Automaten bzw. unendlichen Transitionssystemen sein. Zu den Anwendungen zählt u.a. die Programmverifikation (Model-Checking) und Programmsynthese. Von zentraler Bedeutung sind hierbei Erreichbarkeits- und Äquivalenzprobleme; diese werden für alle genannten Automatentypen behandelt.

Die Vorlesung wird mit einer Screen Recording Software aufgezeichnet und kann i.A. am selben Tag als Video von der Veranstaltungsseite heruntergeladen werden.

Die aufgezeichneten Videos sind in einem Standardformat (AVI für Windows/Mac bzw. DivX für Linux) und können mit den üblichen Playern abgespielt werden. Zusätzlich werden die Folien der Vorlesung im PostScript und PDF Format zur Verfügung gestellt.

Es werden wöchentlich Übungsblätter verteilt, die auch in elektronischer Form über die oben genannte Seite verfügbar sein werden. Die externen Teilnehmer können ihre Lösungen in elektronischer Form einreichen und werden via E-mail betreut.