Towards Scalable Formal Synthesis of Complex Systems

Date:

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

Location:

• Room 804

Abstract:

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):

• Murat Arcak, Professor, University of California, Berkeley
• Calin Belta, Professor, Boston University
• Amin Ben Sassi, Postdoctoral Researcher, University of Colorado, Boulder
• Domitilla Del Vecchio, Associate Professor, Massachusetts Institute of Technology
• Rüdiger Ehlers, Assistant Professor, University of Bremen
• Jie Fu, Postdoctoral Researcher, University of Pennsylvania
• Antoine Girard, Associate Professor, Université de Grenoble
• Sofie Haesaert , PhD Student, Eindhoven University of Technology
• Necmiye Ozay, Assistant Professor, University of Michigan, Ann Arbor
• Jana Tumova, Postdoctoral Researcher, KTH Royal Institute of Technology
• Arjan van der Schaft, Professor, University of Groningen
• Bo Wu, PhD Student, University of Notre Dame
• Majid Zamani, Assistant Professor, Technische Universität München

Schedule: