Prof. Dr. Ernst-Rüdiger Olderog,
Department of Computing Science, FK II, University of Oldenburg,
D-26111 Oldenburg, Germany
In the following we list topics for new PhD projects in SCARE-2, each one with an acronym (for referring to it), the name of the main supervisor who proposes the topic, an abstract, and a description of the planned research. The topics appear in the alphabetic order of the names of the supervisors.
PhD candidates interested in a topic may consult the supervisor for more detailed information. The research direction may be influenced and changed by the doctorands, both in the beginning and during the project. Once a PhD project has started, a second supervisor will be appointed in agreement with the doctorand.
- Synthesis of Remorse Free Strategies for Traffic Sequence Charts (WD1)
- Probably Approximately Correct Automated Formal Modelling (MF1)
- Impact of Fault Models on Realizability and Costs of Region-adherent, Self-stabilizing Distributed Algorithms (OT2)
- Synthesis of Safe Car Controllers (ERO1)
Main supervisor: Werner Damm
Abstract. Traffic Sequence Charts (TSCs) are an extension of Live Sequence Charts (LSCs) offering a concise specification of manoeuvres for highly automated driving. Formally, they can be seen as a visual dialect of a first order linear-time temporal logic, whose visually defined predicates describe traffic snapshots around a bounded environment of the ego car. Message passing elements of LSCs are inherited to describe Car2X communication. The thesis investigates conditions on Traffic Sequence Charts and the underlying world model which allow for the synthesis of remorse-free dominant strategies for the ego car, possibly involving cooperation with other vehicles, to perform the manoeuvres specified in TSCs.
A notion of world models will be defined taking into account the inherent openness, dynamicity, and partial informedness of applications for autonomous highway driving, including dynamic vehicle models. This forms the basis for defining the key concept of remorse- free dominant strategies for TSCs, also taking into account the key notion of robustness. The research will first assume full informedness and investigate cases for which the existence of robust remorse-free dominant strategies is decidable under full information, building on results in AVACS on quasi-decidability of safety properties in non-linear hybrid systems, and derive synthesis procedures for such cases. The work will then follow up one of the two research directions: to provide approximate computational efficient methods for synthesizing remorse- free strategies by performing synthesis on predicate abstractions of the world model, or to investigate the relaxation of full informedness by guaranteeing sufficient levels of environment observations based on realistic sensor models and Car2X communication. The aforementioned two directions could lead to pursuing two related PhD projects.
Main supervisor: Martin Fränzle
Abstract. The traditional formal verification cycle assumes a fixed formal model of the system under design and, if applicable, of its environment. System verification then is pursued based on this “golden device” supplied by the design engineer. This classical notion of design verification, however, lags noticeably behind current trends in cyber-physical system design, where systems become adaptive and may, e.g., learn part of their behaviour only after deployment in situ. Conventional suggestions for dealing with this issue are to either safeguard the system by built-in, fixed —and thus amenable to traditional design verification— interlocking mechanisms overriding any adaptive behaviour or to try verifying the adaption procedures as such. As both approaches do not seem to be able to keep pace with the rapidly increasing integration depth of learning and behavioural adaptation into cyber-physical systems, we do here suggest a complementary new approach: automated mining of formal models featuring rigorously guar- anteed epistemic validity in order to facilitate automatic run-time (re-)verification in presence of substantial behavioural adaptation.
The PhD project will generalise the initial and purpose-specific PAC formal symbolic model learning technique from Fränzle et al. (2015) into a general scheme. It will start from analysing the proposed use-cases of learning and adaptive behaviour in highly automated driving functions in cooperation with the pertinent groups at OFFIS and DLR Brunswick. Based on this, the candidate will develop a generic formal model comprising fixed parts (e.g., the car kinematics) and variable parts subject to learning (e.g., a driving strategy for a certain ma- noeuvre like overtaking). She will then expose techniques for learning an instance of this generic formal model from observations, provide mathematical techniques akin to those from Fränzle et al. (2015) for rigorously quantifying the epistemic validity of the model thus mined, and provide techniques based on quantitative SMT-based verification for robust automatic run-time verification reflecting the statistical nature of the model.
Main supervisor: Ernst-Rüdiger Olderog
Abstract. This PhD project aims at increasing the level of automation in the design of controllers for safe traffic manoeuvres on various types of roads. It will be based on spatio-temporal reasoning, but abstract from the continuous dynamics. As specifications, formulas of a spatio-temporal logic will be taken. Inspiration will be obtained from controller synthesis in discrete event systems and from bounded real-time model checking.
This PhD project will pursue synthesis of car controllers for traffic manoeuvres with the aim of (1) maintaining safety (no collision) and (2) achieving goals such as overtaking within a given time interval if possible (time-bounded liveness). To reduce the complexity of the synthesis, we shall utilise the separation of spatial reasoning from the car dynamics. Starting point for will be an approach by Larsen et al. (2015), and the work by Bochmann et al. (2015), where algorithms are sketched, but automation is still missing. As specifications for which the controllers are synthesised we start from EMLSL formulas of S. Linker (2015).
This research is complementary to PhD project WD1 in that our approach emphasises the decomposition of spatial and dynamic reasoning, whereas WD1 emphasises the need to have a quality measure for strategies even when no winning strategies exist (and then analyses conditions under various levels of informedness for synthesising these).
Main supervisor: Oliver Theel
Abstract. Self-stabilization and region adherence are fault tolerance concepts for building extremely dependable distributed systems: whereas self-stabilization eventually recovers a failed system, region adherence postpones total system failure. Region adherence is a concept that has been recently introduced by the research group of the main supervisor. In the scope of the PhD project, we are interested in analyzing the impact of different fault models on the realization of region-adherent and self-stabilizing systems. We are particularly interested in the identification of fault models that "lie in the intersection," meaning that region-adherent and - at the same time - self-stabilizing systems can be realized and what the resulting costs are. Knowing this fault model class will answer the research question of necessary contexts for the deployment of self-stabilizing, region-adherent systems. On the way to this goal, additional interesting research questions arise, like: (1) How can region-adherent systems be designed? (2) How can distributed algorithms be combined such that they result in region-adherent systems? (3) How can a region-adherent system be refined such that it either operates more
cost-efficiently or with improved reliability? etc. In this sketched research area, a potential candidate might define his/her own research focus.
This PhD project will evaluate ramifications of different fault models on the realizability and costs of distributed algorithms wrt. region adherence, self-stabilization, and - in particular - their co-occurrence. In self-stabilization the impact of specific fault models is often not considered, i.e., faults are unconstrained and may modify a system's state arbitrarily. For region adherence the fault model is of major importance, e.g., more less constrained fault models render a system less region-adherent. We plan to dive into the following research questions: (1) How do different classes of fault models affect the cost for self-stabilization? (2) For which characteristics of applications can self-stabilizing, region-adherent algorithms be constructed? (3) How to exploit knowledge of the fault model when designing self-stabilizing, region-adherent distributed algorithms? (4) How can we identify a sweet spot between region adherence and self-stabilization for a particular application?