Seminar:
Automata Models in Logic

Automata are widely used in logic. The seminar is about the application of automata models (e.g. finite automata, Büchi-automata, alternating automata, …) in specific logics.

Prerequisites: Undergraduate knowledge of automata and logic would be helpful.

There is an initial meeting on 22 October 2015 at 14:50 in room APB/3027. There, topics are assigned to interested students and further organisational matters are covered.

The students taking the seminar should get acquainted with their respective topic, write a report (c. 15 pages) about it, and give a presentation (of 25 minutes) at the end of the semester. They receive indiviual supervision by Prof. Dr.-Ing. Franz Baader, Dr. Marcel Lippmann, Dr. Michel Ludwig, and Francesco Kriegel.

The topics have been assigned as follows:

Student	Topic	Supervisor
Mariëlle Rietdijk	Gerth, Peled, Vardi, Wolper: Simple On-the-fly Automatic Verification of Linear Temporal Logic	Dr. M. Lippmann
Emira Ziberi	Gastin, Oddoux: Fast LTL to Büchi Automata Translation	Dr. M. Lippmann
Ioannis Gerochristos	Pan, Sattler, Vardi: BDD-Based Decision Procedures for K	Dr. M. Ludwig
Atefeh Keshvarzi	Hladik, Sattler: A Translation of Looping Alternating Automata to Description Logic	F. Kriegel
Alexandra Meireles	Baader: Using automata theory for characterizing the semantics of terminological cycles (part about FL0 with gfp-semantics)	Prof. F. Baader
Adrian Nuradiansyah	Baader: Using automata theory for characterizing the semantics of terminological cycles (part about FL0 with descriptive semantics)	Prof. F. Baader
Frederic Dörband	Lutz, Seylan, Wolter: An Automata-Theoretic Approach to Uniform Interpolation and Approximation in the Description Logic EL	Prof. F. Baader

The students are expected to stick to the following schedule.

• in November: mandatory meeting with the supervisor
• 4 January: first complete version of the report due
• 18 January: first complete version of the presentation slides due
• 4 February: give the presentation and participate in the discussion

SWS: –/2/–

This course can be used in the following modules:

• Master-Studiengang (Medien-)Informatik: INF-AQUA (Allgemeine Qualifikationen)
• Diplom-Studiengang Informatik: INF-D-940 (Berufsspezifische Schlüsselkompetenzen)
• Master in Computational Logic: MCL-PCS (Presentation and Communication Skills), MCL-TCSL (Theoretical Computer Science and Logic), MCL-PI (Principles of Inference)
• Diplom-Studiengang Informatik (Studienordnung 2004): Hauptseminar

Will be provided.