Automated Controller Synthesis

In this Focus Group, Hans Fischer Senior Fellow Prof. Anca Muscholl (Laboratoire Bordelais de Recherche en Informatique) collaborates with her hosts Prof. Javier Esparza (Foundations of Software Reliability and Theoretical Computer Science) and Prof. Samarjit Chakraborty (Institute of Real-Time Computer Systems). Further members of the Focus Group are Prof. Matthias Althoff (Cyber-Physical Systems), Prof. Majid Zamani (Hybrid Control Systems), and TUM-IAS Visiting Fellow Dr. habil. Igor Walukiewicz (CNRS, Laboratoire Bordelais de Recherche en Informatique).

Cars, planes, power grids, manufacturing plants, robots, and many other systems, are increasingly controlled by software, running distributedly and involving complex interaction between a large number of components. Certification of software is an essential requirement and can be addressed by algorithmic methods to synthesize controllers guaranteeing system correctness. Controller synthesis techniques produce correct-by-construction solutions that do not require post factum testing or verification. They are therefore a very promising approach to address today’s growing complexity and time-to-market pressures. Distributed systems are particularly challenging in this respect, being highly fault-prone and sensitive to scheduling-dependent errors that can be very difficult to test.

This Focus Group centers its activities around the following problems:

• Simultaneous synthesis of controllers and architecture.

A challenging problem in the context of cyber-physical systems is the simultaneous synthesis of controllers and of the underlying platform or implementation architectures on which they are to be implemented. Techniques for distributed synthesis will prove very helpful here, since they involve the simultaneous synthesis of local controllers.

• Synthesis of distributed monitors.

System monitoring is a prerequisite for control. In programming, monitoring takes the form of assertions: an invalidation of an assertion is the first sign that something has gone wrong in the system and that error recovery should be initiated before problems become more widespread and more visible.  Obtaining scalable algorithms for constructing distributed monitors is a key issue here.

• Distributed synthesis as game solving.

Controller synthesis can be seen as a game between Controller and Environment where the Controller wins if some property is never violated. This game view offers a unifying algorithmic setting for centralized control problems. Identifying settings where solving distributed games for controller synthesis is tractable will lead to a generic algorithmic approach for the certification of complex distributed software.

TUM-IAS funded postdoctoral researcher:
Dr. Denis Kuperberg, Foundations of Software Reliability and Theoretical Computer Science