Seminar Nominale Mengen und Automaten [SemNom] (SoSe 2019)

Dozent Lutz Schröder
Daten Do, 16:15 – 17:45, 00.131-128 (Seminarraum INF8, Cauerstr. 11)

Aus den Grundvorlesungen sind Prinzipien zur Erkennung von Sprachen über endlichen Alphabeten bekannt. In jüngerer Zeit wächst das Interesse an Sprachen über unendlichen Alphabeten, in denen einzelne Buchstaben tatsächliche Datenwerte transportieren können, etwa Datenfelder in XML-Dokumenten, Noncen und Schlüssel in kryptographischen Protokollen, URIs, Sitzungsidentifikatoren uvm. Ein eleganter Formalismus für solche Datensprachen bilden die nominalen Mengen sowie verschiedene hierauf aufbauende Automatenbegriffe. Nominale Mengen spielen außerdem in der Semantik von Sprachen mit Variablenbindung wie etwa lambda-Kalkül und pi-Kalkül eine zentrale Rolle. In diesem Seminar beschäftigen wir uns vor diesem Hintergrund insbesondere mit nominalen Mengen, nominalen Automaten und verschiedenen klassischeren Formen von Automaten über unendlichen Alphabeten und Datensprachen.

Themen

Die folgende Themenliste ist weder notwendigerweise erschöpfend noch wird sie zwingend vollständig abgearbeitet:

  • Mengen, Atome und Symmetrien
  • Nominale Mengen
  • Automaten über unendlichen Alphabeten und Datenalphabeten
  • Registerautomaten
  • Nominale Automaten
  • Nominale Ausdruckskalküle
  • Temporallogik mit Freeze-Quantoren

Vorläufiger Zeitplan

  • 09.05/16.05: Pitts, Kapitel 1 “Permutations”, Fabian Birkmann
  • 16.05/23.05/06.06: Pitts, Kapitel 2 “Support”, Johannes Kern
  • 06.06/13.06: Pitts, Kapitel 3 “Freshness”, Paula Welzenbach
  • 27.06/04.07: Pitts, Kapitel 4 “Name abstraction”, Üsame Cengiz
  • 11.07/18.07: Pitts, Kapitel 5 “Orbit-finiteness”, Florian Deublein
  • 18.07/25.07: Pitts, Kapitel 7 “Inductive definitions”, Renat Tenishev

Literatur

  • A. Pitts, Nominal Sets, CUP, 2013
  • M. Bojanczyk, B. Klin, S. Lasota: Automata theory in nominal sets. Logical Methods in Computer Science 10(3), 2014
  • M. Kaminski, N. Francez: Finite-Memory Automata. Theor. Comput. Sci. 134(2), 1994: 329-363
  • S. Demri, R. Lazic, and A. Sangnier. Model checking Freeze LTL over one-counter automata. In R. Amadio, ed., Foundations of Software Science and Computational Structures, FOSSACS 2008, vol. 4962 of LNCS, pp. 490-504. Springer, 2008.
  • L. Schröder, D. Kozen, S. Milius, T. Wißmann: Nominal Automata with Name Binding. FoSSaCS 2017: 124-142