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@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@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.