[TYPES/announce] PhD/Post-Doc positions at the University of Duisburg-Essen

[Barbara Koenig]

The Theoretical Computer Science Group (Prof. Barbara Koenig) at the
University of Duisburg-Essen, Campus Duisburg (Germany) has two open
PhD positions paid according to TV-L 13 (full-time).

The first position (no. 604-20) is in the DFG project SpeQt ("Spectra
of Behavioural Distances and Quantitative Logics"), which has recently
been granted by the German Research Foundation. This is a joint
project with Prof. Lutz Schröder at the University of
Erlangen-Nürnberg. A project description is attached below.

The second position (no. 605-20) is not associated with a specific
project. The PhD thesis topic will be in the area of modelling and
verification of concurrent systems.

You can apply for one or both positions. For both positions,
candidates at post-doc level can also be considered.

Due to the Covid-19 pandemic universities in Germany are partially
closed. However, there is the possibility to meet and work at the
university, observing the current Corona regulations. There is of
course the possibility to do the job interview virtually.

Requirements
------------

You should have or should be in the process of obtaining an MSc or
equivalent degree (in Computer Science or Mathematics). Prior
knowledge about the topics of the projects is considered an
advantage. Good English speaking and writing skills are demanded, as
well as the willingness to learn German.

For a post-doc position you should have or should be in the process of
obtaining a PhD.

The application deadline is 8th October 2020.

https://www.uni-due.de/theoinf/index_en.php

======================================================================

Your Application
----------------

You can obtain further information by adressing your enquiries to:

Barbara Koenig
barbara_koenig at uni-due.de
tel.: ++49-203-3793397

If you are interested in the position, please send your
application. Your application should include:

* A description of your interest in the position, including your
  motivation and specific qualifications.

* A curriculum vitae, including an abstract of your graduate thesis
  and the name of your supervisor.

* If you are interested in a post-doc position, please include
  a list of your publications and the names of possible referees.

Please send your application directly to me
(barbara_koenig at uni-due.de).


----------------------------------------------------------------------
DFG Project SpeQt - Spectra of Behavioural Distances and Quantitative
Logics
----------------------------------------------------------------------

One of the central topics in the study of concurrent systems are
notions of system equivalence, which define when two given system
states have the same behaviour in a given sense. Classically,
i.e. over relational transition systems, such system semantics range
on a spectrum between branching-time and linear-time equivalences,
with each equivalence reflecting a notion of possible interaction with
systems, and characterized by a dedicated modal logic. In this
setting, equivalences and logics are two-valued, i.e. two states are
either equivalent or inequivalent, and a formula is either satisfied
or not satisfied in a given state. For systems involving quantitative
data, such as probabilities, weights, or more generally values in some
metric space, it has been recognized that quantitative notions of
equivalence, i.e. behavioural distances, and quantitative logics are
more suitable for some purposes, and enable a more fine-grained
analysis. For instance, while two states in Markov chains with small
differences in their transition probabilities are just inequivalent
under two-valued probabilistic bisimilarity, a suitable behavioural
distance will retain the information that the two states are not
exactly equivalent but still quite similar.

As indicated above, behavioural distances by their very nature apply
to settings that deviate from the classical relational model; these
settings are generally less standardized and vary quite widely. This
creates a need for uniform methods that apply to many system types at
once. For branching-time behavioural metrics, we have developed such
methods in earlier work within the framework of universal coalgebra,
which encapsulates system types as functors and systems as coalgebras
for the given type functor. The objective of SpeQt is to additionally
parametrize these methods over the system semantics, thus providing
support for spectra of behavioural distances in coalgebraic
generality.

The key tool we foresee for such a parametrization are graded monads,
which we have successfully used in earlier work to parametrize
two-valued equivalences. Central research goals include game-theoretic
and logical characterization and efficient calculation of
distances. Our results will enable us to derive such logics, games and
algorithms in a principled way for a whole range of different types of
transition systems and for the full spectrum between branching-time
and linear-time semantics. We plan to test and evaluate the resulting
algorithms in case studies centered around conformance testing of
hybrid systems and differential privacy.