Applied Automata Theory WiSe 2012/2013:
======================================

Erforderliche Vorkenntnisse:
============================
Formale Grundlagen der Programmierung
Logik

Lernziele/Kompetenzen:
======================
Controller interagieren andauernd mit ihrer Umgebung, ohne zu terminieren. Die Studierenden modellieren diese reaktiven Systeme mit Automaten und spezifizieren deren Korrektheit mit logischen Formeln. Sie erlernen die zugehörigen Verifikationsalgorithmen und sind in der Lage, die Verfahren auf ähnliche Systemmodelle zu übertragen.

SWS, LP:
========
Vorlesung (4V+2Ü), 8 LP

Sprache:
========
Deutsch (bei Bedarf Englisch)

Anforderungsstufe:
==================
Master (Anfänger)  

Vertiefung:
===========
Algorithmik
Verifikation
Entwicklung eingebetteter Systeme

Inhalt:
=======

Zustandsendliche Systeme:
=========================
Omega-Automaten 
MSO und Satz von Büchi
LTL und Presburger Arithmetik

Rekursive Programme:
====================
Pushdown-Automaten, pre* und post*
Bounded-Context-Switching
Baumautomaten, Satz von Rabin

Parametrisierte Systeme:
========================
Regular-Model-Checking
LTL(MSO)
Quotienten, Abstraktion und Extrapolation

Prüfungsleistungen (Abschluss):
===============================
Mündliche oder schriftliche Abschlussprüfung

Prüfungsleistungen (Zulassungsvoraussetzungen):
===============================================
Lösung von Übungsaufgaben

Medienformen:
=============    
Tafel
Beamer
Skript und Folien zum Download (als pdf)

Literatur:
==========
Wird in der Vorlesung bekannt gegeben