Towards Scalable Formal Synthesis of Complex Systems


  • Majid Zamani, Electrical and Computer Engineering Department, Technische Universität München
  • Antoine Girard, Laboratoire Jean Kuntzmann, Université de Grenoble
  • Alessandro Abate, Computer Science Department, University of Oxford


  • Monday, December 14, 2015 -- 9:00-18:00


  • Room 804


The use of concepts, techniques, and algorithms from the literature on formal verification and synthesis in computer science is becoming increasingly common within the systems and control community. Formal notions such as that of abstraction, or that of simulation relation, which are fundamental in computer science, are increasing their presence in the study of dynamical and control systems. Furthermore, such notions help to improve the understanding of similar concepts that are already in use in systems and control theory, such as that of model reduction (abstraction).

The concept of formal synthesis stands for the process of automated synthesis of controller codes from higher-level temporal logic requirements. The use of temporal logic allows the expression of rich speci cations for time-dependent models, and enables to draw comparisons between themes in classical control theory and their equivalents in computer science. Correspondingly, we invited an interdisciplinary group of control theorists and computer scientists, expert in this domain, to present recent scalable formal synthesis techniques.

These techniques are particularly relevant to address problems dealing with cyber-physical systems, i.e. systems in which computing devices interact with the physical world and vice versa. These techniques can solve many large-scale complex problems that until recently could not be addressed in a methodological way. Furthermore, these approaches have demonstrated their practical relevance with many available model checkers and synthesis tools growing from being exclusively of academic interest to becoming industrially relevant techniques.

Intended Audience:

The proposed workshop will bene t the control community as well as computer science community. We believe that the potential audience of this workshop consists of a large number of CDC participants especially those interested in formal methods and cyber-physical systems. The workshop will be a unique opportunity for an active and productive interaction between control theorists and computer scientists.

Presenters (alphabetic list):