Master's projects

If you are a Computer Science or Embedded Systems student and are looking for a final project, you can have a look at the descriptions below. Contact me if you are interested in one of these projects, or if you have your own idea for a project.

Inferring Automata from a Finite Sample with SAT

The general question is: find an automaton (DFA) for which the accepting language complies with a give sample of words, containing words that must be accepted by the DFA and words that must be rejected. This is a very natural question: the learned automaton describes a set of words, and can be used to predict whether a new string is in the language or not.

However, the problem of finding a minimal DFA consistent with a sample is NP-complete, so the computation time grows quickly with the sample set of strings. There are some existing ideas on how to encode this problem in a Boolean formula, to be solved by SAT solver [1]. The scalability is not great, though.

The goal of this project is to investigate whether better performance can be achieved when the presented data sample has more structure. For example, it may be stored in an observation table, as used in Angluin's L* algorithm. New ideas have to be implemented and experimentally compared to existing SAT encodings.

A possible extension is to investigate whether other automata models, such as non-deterministic automata (NFAs), can be efficiently generated in the same manner.

[1]: Leucker M., Neider D. Learning Minimal Deterministic Automata from Inexperienced Teachers. ISoLA 2012. LNCS, vol 7609. Springer.

Formalising Partial-Order Reduction Theory in Proof Assistants or Other Tools

A common problem in model checking is the explosion of the state space making verification often prohibitively expensive. One technique to partially resolve this problem is partial-order reduction (POR), which was first proposed at the end of the 1980s. Since then, many variants have appeared. Some of these operate on Kripke structures or Labelled Transition Systems and preserve common temporal logics such as LTL or CTL. Others are designed for formalisms such as parity games and try to preserve the winning player.

It turns out however, that correctness proofs for POR are very meticulous, and some even contain mistakes [1,2]. The goal of this project is to apply tools to verify the correctness of these proofs. Several possibilities are tools like Alloy, Coq or Isabelle.

[1]: Thomas Neele, Antti Valmari, Tim A. C. Willemse. A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. Logical Methods in Computer Science, volume 17 (3) pages 8:1-8:27.
[2]: Stephen F. Siegel. What’s Wrong with On-the-Fly Partial Order Reduction. In CAV 2019, volume 11562 of LNCS, pages 478–495, 2019.

Finished projects