Welcome at the chair of Theoretical Computer Science
Our research projects are located in the areas automata theory, logic, computational algebra, information theory, and complexity theory. Currently we are in interested in grammar-based compression, algorithmic group theory, streaming algorithms and algorithmic model theory
Head of group: Prof. Dr. Markus Lohrey
Research areas
Due to the huge amount of data in modern information processing systems, data compression became a key technology in computer science. An important class of compressors are dictionary-based compressors. Famous examples are the Lempel-Ziv compression algorithms. Another class of dictionary-based compressors that received a lot of attention in the past 10 years are grammar-based compressors. The basic idea is to compress a large object (e.g. a text or a large tree structure) by a grammar (e.g. a context-free string or tree grammar) that only produces the initial object. In the best case, this grammar can be exponentially smaller than the initial object.
In many applications, compressed data have to be processed. A typical example is the search for specific patterns in compressed genome data bases. In these applications it is often not feasible to first decompress the data and then process it. We are working on algorithms which directly compute on the grammar instead of decompressing the grammar first. Another research project are techniques for deriving precise quantitative statements on the compression ratio of grammar-based string and tree compressors
Group theory is a part of algebra, where algorithmic problems have been studied since the beginning of the 20th century. Max Dehn defined in his seminal paper from 1911 three decision problems for finitely generated infinite groups: (i) the word problem (does a given word over the group generators evaluate to the group identity?), (ii) the conjugacy problem (do two given words over the group generators represent conjugated group elements?), and (iii)the isomorphism problem (are two finitely presented groups that are given by defining relations isomorphic?) Starting with the work of Novikov and Boone from the 1950's, all three problems turned out to be undecidable in general. On the other hand, for many special classes of groups, Dehn's decision problems and generalizations of these are decidable. In these cases one can ask for the computational complexity of the problems. In recent years, considerable process has been made in this direction by using techniques from computer science (e.g. data compression, rewriting systems, automata theory). In our group, we use for instance techniques from grammar-based compression in order to develop more efficient algorithms for the solution of word problems. Moreover, we look at algorithms for the solution of equations in groups and rational sets in groups
Streaming algorithms are algorithms that do not get random access on the input data. Instead, the algorithm receives one new symbol/data value at each time instant. Streaming algorithms are important in big data analytics, where random access on the whole input is not feasible. In recent years we developed an automata theoretic approach to streaming algorithms. Our focus was on deterministic and randomized sliding window streaming algorithms for formal languages (in particular, regular languages and context-free languages), where only the last n data items are relevant at each time instant (n is the window size)
Model theory is a classical area in mathematical logic, which studies the interplay between the algebraic and logical properties of structures. For applications in computer science, this missing algorithmic focus in model theory is an obstacle. Algorithmic model theory compensates this. Its focus is on structures that are defined by abstract machine models, like finite automata or pushdown machines. Whereas classical model theory is mainly concerned with first-order logic, algorithmic model theory also studies logics that are tailored towards applications in areas like automatic verification or database theory. Examples for such a logics are temporal logics like LTL and CTL, or the highly expressive monadic second order logic. These logics can expressive important system properties like reachability or fairness.
Current research topics at the chair for Theoretical Computer Science include the algorithmic theory of automatic structures and temporal logics with numerical constraints
Teaching
| Advanced Logic (M.Sc. Computer Science) | 43THI0031V | Moodle | Unisono |
| Übungen zu Advanced Logic / Practise Advanced Logic (M.Sc. Computer Science) | 43THI0032V | Unisono | |
| Algorithmik II / Algorithmics II (M.Sc. Computer Science) | 43THI0023V | Moodle | Unisono |
| Übungen zu Algorithmik II / Practise Algorithmics II (M.Sc. Computer Science) | 43THI0024V | Unisono | |
|
Formale Sprachen und Automaten / Formal Languages and Automata (B.Sc. Informatik) | 43THI0035V |
Moodle | Unisono |
| Übung zu Formale Sprachen und Automaten / Practise Formal Languages and Automata (B.Sc. Informatik) | 43THI0036V | Unisono | |
| Quantum Complexity Theory (M.Sc. Computer Science) | 43THI0037V | Moodle | Unisono |
| Übung zu Quantum Complexity Theory / Practise Quantum Complexity Theory (M.Sc. Computer Science) | 43THI0038V | Unisono |
| Algorithmik I / Algorithmics I (M.Sc. Computer Science) | 43THI0021V | Moodle | Unisono |
| Übungen zu Algorithmik I / Practise Algorithmics I (M.Sc. Computer Science) | 43THI0022V | Unisono | |
| Berechenbarkeit und Logik / Computability and Logic (B.Sc. Informatik) | 43THI0037V | Moodle | Unisono |
| Übung Berechenbarkeit und Logik / Practise Computability and Logic (B.Sc. Informatik) | 43THI0038V | Unisono | |
| Cutting Edge Research (M.Sc. Computer Science) | 43THI0039V | Moodle | Unisono |
| Komplexitätstheorie I/ Complexity Theory I (M.Sc. Computer Science) | 43THI0028V | Moodle | Unisono |
| Übungen zu Komplexitätstheorie I / Practise Complexity Theory I (M.Sc. Computer Science) | 43THI0029V | Unisono | |
| Seminar Theoretische Informatik / Seminar Theoretical Computer Science (M.Sc. Computer Science) | 43THI0016V | Moodle | Unisono |
Compression of finite structures using automata (topic for master thesis)
Automatic structure are relational structures that are represented in a certain sense by finite automata. Usually, these structures are assumed to be infinite. There is a rich theory of automatic structures relating them to areas like mathematical logic and computability. The concept of automatic structures can be also used in order to represent finite structures in a compressed way by automata. The goal of the project is to compare automatic representations of finite structures with related concepts like BDDs (binary decision diagrams) and to investigate the complexity of algorithmic problems for finite structures when the input structure is given by finite automata.
Using SAT solver for algorithmic problems on permutation groups (topic for master thesis)
A permutation on the set {1, 2,…, n} is just a bijective (one-to-one) function on {1, 2,…, n}. The set of all permutations on {1, 2,…, n} form a group, the so-called symmetric group on {1, 2,…, n}, which is also denoted by Sym(n). The multiplication in Sym(n) is just the composition of functions. An important computational problem in this context is the so-called permutation group membership problem:- The input is: a number n, a permutation f from Sym(n), and a finite subset S of Sym(n).- The question is whether f can be written as a product (of arbitrary length) of permutations from S.The classical Schreier-Sims algorithm solves this problem in polynomial time. A more difficult problem is the so-called length problem for permutation groups: The input is the same as in the above permutation group membership problem plus an additional number m. The question is then whether f can be written as a product of permutations from S, where the product must have length at most m. This problem is quite difficult to solve: it is an NP-complete problem (Even and Goldreich 1981) The goal of the project is to explore the use of SAT solver in order to solve instances of the above length problem. SAT solver a software tools that are used for checking whether a given boolean formula is satisfiable (the so-called SAT problem), i.e., whether one can assign truth values to the variables in the formula such that the fomula becomes true. It is not difficult to translate an instance of the length problem for permutation groups into a SAT problem, which then can be attacked with a SAT solver. There are several freely available SAT solver that can be used for this.