Why would you do a PhD in the Automating CPS Design research group?

We have job openings for scientific employee positions from time to time, which are suitable for doing a PhD while having the position. The task that you have when holding such positions include performing research on the topics on the group and helping with teaching of courses taught by the other members of the group. The research performed in this context is the one that will later get you your PhD degree, and the head of the group takes care that the concrete research work done is suitable for getting a PhD later in case of sufficient results.

There are a good number of reasons to apply for an open position:

  • In the research group, we take care that the various obligations that come with a scientific employee position do not become too exhessive to prevent you from making progress with your research.
  • We have plenty of national and international contacts to make research visits of other research groups and similar activities possible.
  • We work on publications for high-quality venues that are suitable for preparing academic as well as industrial carrers.
  • Our work combines theory and practice; it is not only foundational, but applied at the same time, as we implement our approaches in prototype tools and apply them to case studies.
  • * Out work is very diverse. It spans automata theory as well as machine learning, embedded systems monitoring, and hardware aspects of embedded systems. There are many questions in the field spanned by these topical anchors, and there is surely something for you as well!

To enable you to succeed in this context, you should have acquired some needed skills during your past studies (or before that):

  • The ability to introduce yourself to new areas of research by reading a suitable textbook. We import concepts and algorithms from adjacent domains of research into our own work. Normally, there are no courses available on the respective topic at TU Clausthal, so we (have to) resort to primary and secondary literature here.
  • You should not be afraid of formal notation. For the eventual publication of ideas at reputable international venues, they need to be clearly expressed. Normally, this involves using formal notation to bring the point across. Ideally, you did not acquire a habit of skipping the formal parts when reading texts in the past and you should be willing to work on using formal notation to improve your writing skills.
  • The ability to think about computational problems and make observations on previous approaches to tackling a problem. This may involve observing the strengths and weaknesses of existing tools/implementations, as well as thinking about an algorithmic solution to a problem by analyzing its main ideas.

To exemplify how we combine theory and practice in our research group, consider the following projects that have been performed by members of the group:

 

High-Level Robot Control: There is a lot of work on automating the design process of high-level robot controllers. These coordinate the various tasks of the robot and trigger low-level controllers that for example steer the robot to a different location. When automating the design process, the user of the robot only has to write down what the robot should do, and the controller is computed automatically. This is highly advantegous in scenarios with frequently changing specifications. For robots operating in environments that carry probabilities, such as the probability of a robot breaking, high-level robot controllers should maximize the probability of satisfying the specification.

Unfortunately, it turns out that with the commonly used specification formalisms in this context, maximizing these probabilities makes no sense. For instance, if the robot has a fixed positive probability of breaking at every time step, it will almost surely eventual break and not satisfy its specification henceforth. So all high-level controllers are equally bad in this case, and no algorithm for computing a "good" one yields a usable robot controller.

In a work published at the 55th IEEE Conference on Decision and Control (CDC 2016), we came up with a way to solve this problem. We researched a way to capture the intuition of the engineers' thought process when designing controllers for a probabilistic environment into an optimization objective that can then be used to synthesize a reasonable controller. The idea used was that an engineeer-made controller is both risk-averse in that the controller will prefer actions with a low risk of breaking, but at the same time the robot controller is always optimistic that the respective next goal is reached and hence plans ahead for the time afterwards at each step of its execution. We concretized this intuition into a algorithm for performing synthesis. The algorithm was implemented in the academic tool ramps, which can be downloaded here. You can also find a video of the synthesized robot behavior here. Note that as a foundational work, we used a very simple simulation that show the effect of the algorithm rather than a real-world scenario.

Neural Network Verification: In many applications, machine-learned models need to be verified before they can be used productively in the field. Unfortunately, doing so is provably difficult in many cases. The reason is that the non-linearities that make machine learning powerful at the same time make verification difficult. If the network behaviour was only linear, verification would be no problem as most verification problems would then become linear programming problems, which are known to be solvable efficiently.

In a work published at the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), we developed a way to approximate the behavior of an artificial neural network using a suitable linear approximation of the behavior of individual nodes. We combined the idea with a search process of possible network behavior in order to get a verification approach that was - at the time - state of the art. The work also introduced a case study that is still in use.

Both examples show that our work combines theory and practice. By the way, don't be worried if you didn't understand these project descriptions completely. Most research work starts from existing works, and if you don't know them (yet), where exactly the novel ideas lie can be a bit tricky to grasp.

When should you apply for a PhD position at the ACPS Group?

  • Whenever you are interested in working on such problems towards a PhD degreen and in an environment that is intellectually stimulating.
  • Whenever you think that the combination of theory and practice that our group offers is the right to prepare you for a carrer in solving interesting computer science problems that can keep you intellectually satisfied until retirement.
  • Whenever you have a Master's degree in computer science and remember at least the basics in the theoretical aspects of this field.

And if you have any questions, please contact Rüdiger Ehlers.