# Bachelor thesis assignments

Below you find a number of examples of potential assignments for a bachelor thesis. In general there are far more assignments than can
be listed here. It is always more fruitful to do a bachelor thesis assignment that matches your interests. Therefore, I invite you
to discuss your particular desires with me.

###
Find an optimal solving recipe for Rubick's 2x2 cube.

Using mCRL2 it is possible to model Rubick's cubes. For the 2x2 cube, the statespace is
sufficiently small to be generated completely, and hence it is straightforward to calculate using
mCRL2 the optimal sequence of turns required to solve the this cube. An intriguing question is whether
an optimal or near optimal recipe can be devised to solve the puzzle, given that the complete
state space is known. An initial investigation reveals that the 'standard' approach to solve cubes
is not particularly optimal. Doing the upper corners last requires almost as many turns as are
required to solve any 2x2 Rubick's cube.
###
Implementing a fast graph positioning algorithm.

The tool ltsgraph in the mcrl2 toolset is used to visualize directed graphs. It
uses a simple spring-attraction algorithm to position edges and vertices. Its complexity is quadratic per contraction
step of the algorithm and For large graphs the algorithm is
far too slow. The assignment is to find and implement a faster algorithm to poaition the states.
###
Design and possibly implement a fast parallel aterm library.

The aterm library maintains terms that are maximally shared in memory. When terms are constructed, it is checked whether
they already exist, via a hash table, and then inserted in a term database. In a parallel setting it is not really
possible to guard every access to the hash table with a mutex, as performance will drop too much. The question is whether
it is possible to design a hash table access and term creation scheme that avoids synchronization as much as possible,
such that a parallel hash table implementation running on multiple processors will be faster than the standard available
implementation for one processor.
###
Translate CIF to mCRL2.

At the department of mechanical engineering the specification language CIF is used. This language cannot do evaluation
of properties. The toolset mcrl2 toolset can provide verifications. There is a translator
from CIF to mCRL2, but it is not optimal if there are many parallel processes. In this assignment it is requested to
make a better translator. This assignment is together with dr.ir. Michel Reniers at the department of Mechanical Engineering.
If you visit me to discuss potential bachelor thesis assignments, I appreciate if you can bring a list of attended courses.

Return to the homepage of the Formal System Analysis group.
Return to the homepage of J.F. Groote.