Automata over infinite alphabets

Logic & Computation

Automata theory is one of the pillars of computer science, aiming at a systematic understanding of computation via machine models. In the 60 years of its existence, it has been extensively investigated and applied to a wide spectrum of areas, ranging from linguistics to software specification and verification. Traditionally, automata theory examines languages defined over finite alphabets. However, this restriction has recently been seen as limiting, specifically in frameworks examining alphabets of very large or unbounded sizes, such as XML analysis or verification of programs with dynamic resource allocation. This course will examine automata formalisms developed in the last 20 years to attack the infinite alphabet challenge. We shall start off by examining the notion of register automata: a bounded-memory machine proposed as an analogue to finite-state automata. We will then proceed to their extension with pushdown stack, seen as the infinite alphabet counterpart of pushdown automata, and then examine even more expressive models, whose emptiness problems touch the boundaries of decidable computation.

First week
09:00 - 10:30 - slot 1