What are the practical uses of infinity

Automata theory and its applications

Dr. Thomas Schneider
kind of event
K4, Master's Supplement, Elective Area: Special Topics in Logic
time and place
Mon. 12:30 pm - 2:00 pm, MZH 1470
Wed. 8: 30-10: 00, SFG 2020
See also entry in the course catalog for computer science for the 2014 summer semester
Additional appointments
Thursday, July 17, 8:30 am-10:00am, MZH 1110
Thursday, July 17, 12:30 pm - 2:00 pm, Cartesium 2.43 (meeting room 2nd floor)
for this failure on July 21st and July 23rd

Brief description

Theoretical automata techniques have useful applications in computer science: they can be used, for example, to check security-relevant properties of a system (verification), define robust XML languages ​​or evaluate queries on XML trees. To do this, one has to generalize the standard concept of finite automata to words by moving from finite words to infinite words or trees. This extension of the term automaton as well as the related theoretical results and practical applications are the subject of this course.

Brief overview of the topics:

  • Repetition of finite automata and formal languages
    Applications: text search, pattern search, text replacement
  • Automata on finite trees
    Application: Inclusion in term rewriting systems
    Application: XML schema languages
  • Automata on infinite words
    Application: verification and temporal logic (LTL)
  • Automata on infinite trees
    Application: verification and temporal logic (CTL)

Knowledge from the "Theoretical Computer Science 1" course is helpful, but is not required - we will briefly review the most important aspects at the beginning.



Introduction 4 per page
Part 1 4 per page (version from May 20, 10:30 a.m., small corrections F. 51–53)
Part 2 4 per page (version from May 27, 12:30 p.m.)
Part 3 4 per page (version from July 16, 12:05 p.m.)
Part 4 4 per page (version from July 16, 4:00 p.m.)

Exercise sheets

Exercise sheet 1 (submitted on May 5th)
Exercise sheet 2 (hand in on May 19)
Exercise sheet 3 (submitted on June 2nd)
Exercise sheet 4 (submitted on June 23rd)
Exercise sheet 5 (submitted on July 9th)
Exercise sheet 6 (meeting on July 17th)

More material

XML, DTDs and validation

conference.xml with invalid DTD validation result
conference2.xml with valid DTD and valid XML document - validation result
conference3.xml with valid DTD, but invalid XML document - validation result
External link to the W3C validator

Minimization of Büchi machines

References to read (PDFs are also in StudIP):
  1. Sudeep Juvekar, Nir Piterman: Minimizing Generalized Büchi Automata. Proc. of CAV-06, vol 4144 of LNCS, pp. 45-58, Springer-Verlag, 2006. SpringerLink
  2. Christof Löding: Efficient minimization of deterministic weak ω-automata. Information Processing Letters, 79 (2001) 105-109. ScienceDirect

AG Theory of Artificial Intelligence July 16, 2014 Thomas Schneider