Efficient engineering of supervisory controllers

Many cyber-physical systems are safety-critical: failures or malfunctions may have serious consequences to people's lives or the environment. Therefore, correct functioning of cyber-physical systems is vital. Examples of cyber-physical systems include medical equipment, production systems, and agricultural systems.

A cyber-physical system is steered by a supervisory controller, also known as a supervisor. The supervisor is responsible for the high-level control strategy, making sure all components cooperate and the system properly performs its tasks. Supervisors can be obtained through synthesis-based engineering, which is based around the use of mathematical models. These models describe the uncontrolled system behavior (what the system can do) and a model of the requirements (what the system should (not) do).

By applying supervisor synthesis to these models, a supervisor is algorithmically obtained. This supervisor is correct-by-construction: When the system is steered by this supervisor, the requirements are always adhered to, and some more behavioral properties are satisfied. The modeling and synthesis framework is called supervisory control theory.

Contributions

For his PhD research, Sander Thuijsman has made several contributions to the field of synthesis-based engineering. These contributions aid the ease of use, applicability, and efficiency of supervisory control theory. Indirectly, this thesis contributes to the correct functioning of cyber-physical systems. The contributions cover three separate aspects of supervisory control theory.

Transformational approaches in supervisory control

Typically, cyber-physical systems evolve over time. For example, a new bicycle detection sensor may be added to an existing traffic light system. As a result, the supervisor will progress to several iterations. Consequently, algorithmic computations that are applied to the system during synthesis-based engineering need to be applied for each iteration.

Traditionally, the computations are repeated from scratch for each iteration. These computations may take a long time to complete. For his thesis, Thuijsman studied transformational approaches. In such approaches the results from previous computations are reused in new computations every time the system evolves. The idea is that in this way the algorithmic results are more efficiently obtained.

Supervisory control for product lines

A product line describes a collection of products that share commonalities, but also allow variability between them. For example, a coffee machine that has variants that do or do not have the ability to pour milk or tea. There may be many possible configurations for a product in a product line.

In his PhD work, Thuijsman studied how to apply synthesis-based engineering for product lines. Models were generated that are suitable for supervisor synthesis, and the obtained supervisor can correctly control the system for all possible configurations.

Efficient symbolic supervisor synthesis.

When the size of a system grows, the computational effort required for supervisor synthesis grows exponentially. To mitigate this, the system can symbolically be represented using binary decision diagrams (BDDs), and supervisor synthesis can be applied to this symbolic representation.

Minor changes in how symbolic synthesis is algorithmically performed, or the settings with which it is initiated, can have a major impact on the required time and memory for the computation. Thuijsman explored several approaches to efficiently perform symbolic supervisor synthesis.

Title of PhD thesis: Efficient engineering of supervisory controllers. Supervisors: Michel Reniers (TU/e) and Kai Cai (Osaka Metropolitan University)