Computer Science


technical diagram

Theory and Applications of Formal Systems

The research of the TAFS Group covers a relatively wide range of established and emerging fields in Theoretical Computer Science, including mathematical logic, formal languages, computability and complexity theory, numerical analysis, cryptography, geometric computation, algorithmic learning theory and energy-efficient scheduling.

Group members

Dr Paul Bell is mainly interested in computability and complexity theory and studying the decidability of problems related to algebraic structures, hybrid systems and formal languages. He has shown many problems to be undecidable in these areas mainly through reductions from modifications of existing undecidable problems such as the Post correspondence problem and Hilbert's tenth problem. For decidable problems, he is also interested in studying their computational complexity and thus tractability. He has written several papers in international conferences and journals of theoretical computer science on these topics.

He is also interested in scheduling problems and online algorithms related to multiprocessor systems. For such problems, the goal is to find an optimal dispatching of jobs to processors and optimal processor speeds that will minimise the total amount of energy used.

These are both currently very active areas of research with applications to many areas of Computer Science and Mathematics.

Dr Walter Hussak is interested in non-classical temporal logics and their application to the specification of concurrency. His main research is in the decidability and expressiveness of fragments of first-order temporal logics, and the application of both propositional and first-order temporal logics to specifying the infinite execution of cases of transactional concurrency. Much of the work in first-order temporal logic draws on results from the classical decision problem of mathematical logic. It has concerned the 'monodic' fragment of first-order temporal logic which is the main known decidable fragment. The classical part of the existing decidability result has been extended to fragments which include both time-dependent and time-independent function symbols, and the temporal part to fragments which include grammar operators and propositional quantification. The latter improves on the expressiveness of the original monodic fragment in providing greater coverage of the full classical two-sorted temporal logic. The monodic fragment has been shown to be suitable for specifying schedules of concurrent transactions accessing unlimited data, in which the main correctness condition of serializability is expressed in a first-order manner and is decidable.

He is also interested in graph theory, particularly the reduction of infinite transactional conflict graphs to finite graphs, and symmetric collections of disjoint Hamilton cycles in star graphs for the design of high-performance resilient interconnection network topologies.

Dr Robert Mercas is mainly interested in combinatorics and algorithms on strings. He is also interested in formal languages and automata theory, trace monoids, and pattern inference. His combinatorial work focuses on different variations related to sequences and their characterisation within different settings. Avoidability within sequences is one of his main research interests. 

On the algorithmical side, he is interested in approximation algorithms that have a strong motivation in bioinformatics and other application areas.

He has so far written several papers for different international conferences and journals of theoretical computer science on these topics. Although theoretical, these research areas are quite active and are directly related to real-life applications and phenomena. 

Dr Daniel Reidenbach is mainly interested in two major subareas of theoretical computer science: algorithmic learning theory and formal languages. In particular, his research deals with patterns in strings of symbols, their underlying mathematical theory and the problem of computing such patterns. These topics show strong connections to various other fields in theoretical computer science and discrete mathematics, such as computability theory, combinatorics on words, and complexity theory.

Many of his recent results are related to so-called pattern languages, i.e., sets of strings that all follow a given pattern. His achievements include:

  • deep insights into the algorithmic learnability of pattern languages, a prominent field of research in algorithmic learning theory
  • several results on the equivalence and inclusion problems for pattern languages
  • establishing a novel field of research in combinatorics on words
  • studying the ambiguity of morphisms in free monoids

Some of these results solved longstanding problems, and the corresponding publications won prestigious academic awards at international conferences in theoretical computer science.

Dr Ana Salagean is interested in sequences used for cryptography, and especially for stream ciphers. Previously she has worked in the area of error-correcting codes, and she is still very interested in results that combine coding theory and cryptography. Her current research focuses on the following directions:

  • Linear complexity, k-error linear complexity and balancedness. These parameters are some of the measures used for evaluating the quality of pseudorandom sequences. Our results include bounds on these parameters as well as algorithms for computing these parameters
  • Linear feedback shift registers (LFSR) are hardware devices used to produce so called "pseudo-noise" bit sequences. They are used as building blocks in many stream ciphers, as well as a variety of other applications. We exploit the two different LFSR variants: Fibonacci and Galois for obtaining sequences at a faster rate or with specific properties
  • Higher order differential attacks (such as the cube attack) have been used to attack several ciphers which can be represented as polynomials where some variables are secret and some are "tweakable" i.e. can be manipulated by the attacker. We work on generalising and extending this attack technique