AAU logo

Department of Computer Science

Ph.D. defence by Zhengkui Zhang

Zhengkui Zhang will defend his thesis “Time and Cost Optimization of Cyber-Physical Systems by Distributed Reachability Analysis” on Tuesday 28rd of March 2017, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300

Last modified: 28.02.2017

Zhengkui Zhang will defend his thesis:

Time and Cost Optimization of Cyber-Physical Systems by Distributed Reachability Analysis

The defence takes place on Tuesday 28rd of March 2017, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300



There is no doubt that real-time systems are ubiquitous in our information society. They are the brains of many critical systems, and becoming more pervasive with the rise of cyber-physical systems and industry 4.0. Incorrect designs of those critical systems can result in a significant loss of money for re-design and fixing, or more seriously in catastrophe for system safety. The challenge summons a new development methodology that should be more rigorous and precise. Therefore "model-based systems engineering" based on a series of automated model-based formal methods has been proposed to facilitate design, analysis, optimization, verification and validation activities. 

Network of timed automata is an elegant framework for modeling real-time behaviors, constraints and interactions between concurrent components of a real-time reactive system in a natural way. Timed automata have been widely used as the input models for real-time model checking. Time optimal reachability analysis is a novel use of timed automata for solving scheduling and planning problems in a static environment. However it also inherits state-space explosion from model checking. The thesis develops distributed algorithms for time optimal reachability to efficiently accelerate finding the optimal results and battle the state-space explosion.

An extended form of time optimal scheduling is multi-objective scheduling regarding a variety of quantitative objectives. The thesis extends timed automata with discrete prices on transitions, and develops algorithms for Pareto optimal reachability analysis to compute a set of schedules that are in Pareto optimum. Engineers can choose a schedule that is close to their preference andoptimized for all objectives in the best balance. 

Stochastic hybrid automata and timed game automata are extended formalisms of timed automata that are able to model more complexities about a real-time reactive system as well as handling unpredictable environments. They are the input models for statistical model checking and controller synthesis separately. The thesis integrates controller synthesis and (statistical) model checking, such that users can conveniently verify a synthesized strategy for additional correctness properties by model checking, and evaluate the performance aspects of the strategy by statistical model checking.


Associate Professor Josva Kleist, Aalborg University

Senior Researcher Radu Mateescu, Inria Grenoble 

Associate Professor Bernhard Klaus Aicherning, Graz University of Technology.

Supervisors are Professor Kim Guldstrand Larsen and Associate Professor Brian Nielsen.

Moderator is Associate Professor Ulrik Nyman.

All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.

All news