Theoretical computer science

Advancing theory, addressing fundamental questions in computer science and strengthening connections to other science and engineering disciplines.

This theme focuses on fundamental aspects of the theory of Computer Science, encompassing a range of established and emerging fields including formal language theory, complexity theory, algorithmic learning and automata theory.

Our research uses techniques from several areas of Computer Science, Mathematics and Engineering, including combinatorics, linear algebra, graph theory, computational reduction, algebraic and computational number theory, dynamical systems, symbolic dynamics, and complex analysis, among others.

Formal language theory

Formal language theory underpins the analysis of problems from a wide range of areas in Computer Science and Mathematical Logic. Formal language theory allows us to express syntactic and semantic properties of programming languages and their compilers, define complexity classes, prove hardness results of computational problems, and to reason about abstract notions via mathematical logic. Automated verification and synthesis problems for programming languages can often be understood via symbolic dynamics and their analysis requires understanding the combinatorial properties of formal languages, for example. There is a rich theory related to combinatorics on words, which finds applications in studying a wide range of other problems. Other topics studied within this strand include regular, context-free and context-sensitive languages, membership and ambiguity problems, pattern languages, and connections to automata theory and mathematical combinatorics.

Complexity theory

Two fundamental issues related to algorithmic problems are of paramount importance in Computer Science, that of computability and complexity theory. Computability theory investigates computational problems and determines under what conditions an algorithm exists to solve them. One of the earliest and deepest theorems of Computer Science was shown by Alan Turing back in the 1930s; namely that there exist problems for which no algorithm exists to solve them (known as undecidable problems). Even for those problems that are solvable, in some instances we can prove that they are intractable, and no efficient algorithm for solving them exists.

In this strand, we study algorithmic problems from a wide domain of applications, in Mathematics, Computer Science, and Engineering. Using notions of algorithmic reduction, we can show that certain problems are intractable, or else derive efficient algorithms and data structures that can give positive solutions to such problems under certain conditions.

We are interested in algorithmic problems from a range of real-life application domains, including connections to problems in automated verification of systems, hybrid dynamical systems, online multi-processor scheduling algorithms and randomised algorithms.

Automata theory

Automata theory was one of the founding concepts of Computer Science, and still enjoys a rich and active community of researchers. Our group researches fundamental problems in probabilistic, quantum, cellular, and hybrid automata, as well as more general and extended models of nonstandard computational models and linear dynamical systems. Such problems are related to the automated verification of computational systems and the synthesis of constraints satisfying certain safety and liveness criteria, and allow us to reason about properties of formally defined systems or computer programs.

The investigation of such disparate models of computation allows us to derive a deeper understanding of the notion of what can be computed and to understand how computation is possible, even in nature.