Research Training Group SCARE

PhD Projects in SCARE-2

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

Acronym: WD1

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.

Planned Research.

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. 

Probably Approximately Correct Automated Formal Modelling

Acronym: MF1

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.

Planned Research. 

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. 

Verifying Infinite-state Graph Transformation Systems

Acronym: AH1

Main supervisor: Annegret Habel

Abstract. Graph transformation systems have been emphasized as suitable tool for modelling systems. In this PhD project, graph transformation systems under adverse conditions shall be investigated: the system and the environment describing the adverse conditions shall be modelled by graph transformation systems,  the interaction between them by a finite automaton describing the set of accepted sequences of rule names, and the specification by a temporal graph condition corresponding to a temporal formula.

A theory on algorithmic verification of infinite-state graph transformation systems in the sense of Abdulla et al. shall be given: For a graph transformation system and a temporal graph condition, a labelled transition system shall be constructed. Criteria for well-formedness shall be developed and, for the case of non-well-formedness, semi-algorithms for correctness shall be given. 

 

Planned Research. 

In the automata-theoretic approach, both the system and the property are represented or translated into automata so that checking the property is reduced to the emptiness problem of languages or the reachability problem of states, respectively. In this PhD project, a labeled transition system shall be constructed from the system and the property: Given a graph transformation system ℛ and a temporal graph condition tc, a construction of a labeled transition system shall be given using the constructions of weakest preconditions and strongest postconditions: For a graph condition c, underlying the given temporal graph condition tc, we construct the weakest preconditions and strongest postconditions for rules ρ ∈ ℛ and the initial or constructed graph conditions, until no new graph conditions can be constructed. It shall be investigated under which conditions the constructed labeled transition system is well-formed in the sense of Abdulla et al. For arbitrary labeled transition systems, semi-algorithms for correctness shall be considered. By product construction, the adverse conditions represented by a finite automaton, shall be integrated. Infinite-state verification shall be illustrated at a larger example, e.g., a railroad system or a car platooning system.

Interpretable machine learning models for learning under adverse conditions

Acronym: OK3

Main supervisor: Oliver Kramer

Abstract. Complex machine learning models, such as deep neural networks, achieve outstanding predictive performance in a wide range of applications like visual object recognition or speech perception. However, deep learning models are usually black box models and do not allow the interpretation of internal decision processes. Further, adverse conditions like the presence of noise or bias increase the challenge for learning reliable predictive models. In such scenarios, interpretable models play an important role: We assume that an increase of reliability in learning scenarios under adverse conditions can be achieved by integrating mechanisms of interpretability. For example, internal processes can be documented for humans and allow human intervention. In recent studies, interpretable machine learning models have been developed that add valuable information for human understanding of machine decisions.

 

Planned Research. 

The objective of the proposed PhD project OK3 aims at developing and enhancing interpretable machine learning perception models with emphasis on disturbed and noisy data.

Dynamic Reconfiguration as Means to Reducing the Degradation of Components of Robust ICT Systems being Subject to Ageing Effects

Acronym: WN2

Main supervisor: Wolfgang Nebel

 

Abstract. Dynamic partially reconfigurable circuits are field-programmable systems that allow for the personalisation of new functionality (mapping) for parts of their circuit structure (reconfigurable areas) at runtime. These circuits will in future, that is below the 22 nm process technology, suffer from increased ageing and degradation due to physical effects, too. The properties of these circuits and therefore the including systems (Sys) are thus exposed to changes over time. The magnitude of such changes depends on conditions in the environment (Env) of the system. At the same time the reconfigurability provides high flexibility in terms of mapping functions to hardware resources (reconfigurable areas). This PhD proposal will investigate methodologies that mask degradations effects specifically in behaviour of timing by remapping. Functionality can, e.g., be moved from a (degraded) circuitry into another (less degraded) circuitry. Timing uncritical functionalities could still utilize the already degraded parts of the circuit. This PhD proposal examines applicable methodologies for monitoring the degradation and dynamic control of reconfiguration at runtime.

 

Planned Research.

Based on existing methodologies for load-dependent modeling of temperature and energy consumption of a system, this PhD proposal shall enhance existing ageing models on application specific integrated circuits (ASICs) for reconfigurable circuits. Next, these models shall be integrated into the OSSS+R/Fossy system, to enable a simulative assessment of dynamic replacement strategies and circuit partitions, too. Optionally, a concept for a runtime system to enable the required monitoring and the replacement strategies shall be developed and implemented in a prototype.

Distributed Synthesis for Systems with
Dynamic Concurrency

Acronym: ERO2

Main supervisor: Ernst-Rüdiger Olderog

 

Abstract. This PhD project considers the problem of distributed synthesis for systems with dynamic and possibly unbounded concurrency. The mathematical backbone will be the recently introduced Petri games, where the tokens model environment and system players. Applications can be found in robot control for smart manufacturing, where the environment can generate unboundedly many orders, which are then considered as system players that need to be processed by the robots so that the resulting products satisfy some specification property. Adverse conditions are the dynamically changing concurrency, the limited information of the robots about each other, and the possibility that robots may turn out to be defective. In general the synthesis problem is undecidable for unbounded Petri games, whereas for bounded ones the problem has been proven decidable under some assumptions: see below. The aim of the PhD project is to extend a previously achieved synthesis result for bounded Petri games to patterns of Petri games with unboundedly many players. 

 

Planned Research. 

Finkbeiner and Olderog (2014) showed that for Petri games with boundedly many system players, a single environment player, and a local safety objective, deciding the existence of a winning strategy for the system players is EXPTIME-complete. Attempting to overcome the assumptions of this decidability result opens various lines of research. This PhD project will pursue one such direction. It will investigate Petri games with dynamically changing, possibly unbounded numbers of concurrently active players. This is beyond reach of the Pnueli-Rosner model and Zielonka automata. Since for unbounded Petri games the existence of winning strategy is general undecidable, the PhD project shall look for restrictions, e.g., patterns of applications, where the problem of distributed synthesis can be proven to be decidable. Besides this theoretical work, the thesis will also address the algorithmic aspects, e.g., by extending the synthesis tool ADAM. Case studies from manufacturing and workflow scenarios with dynamic concurrency will serve to show the applicability of the approach.

Impact of Fault Models on Realizability and Costs of Region-adherent, Self-stabilizing Distributed Algorithms

Acronym: OT2

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.

 

Planned Research.

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?