Direkt zum Inhalt
Direkt zum Inhalt

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

Chip

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.

Members

Prof. Lohrey

Univ.-Prof. Dr. Markus Lohrey

Professor*in
Personal profile photo

Alexander Thumm

Wissenschaftliche*r Mitarbeiter*in
Personal profile photo

Julio Cesar Juarez Xochitemol M.Sc.

Wissenschaftliche*r Mitarbeiter*in
Personal profile photo

Dr. Rahul Jain

Wissenschaftliche*r Mitarbeiter*in
Personal profile photo

Andreas Rosowski M.Sc.

Wissenschaftliche*r Mitarbeiter*in