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

Publication by the Focus Group

2018

  • Esparza, Javier; Kuperberg, Denis; Muscholl, Anca; Walukiewicz, Igor: Soundness in negotiations. Logical Methods in Computer Science ; Volume 14, 2018, Issue 1 ; 1860-5974 mehr…

2017

  • Esparza, Javier; Muscholl, Anca; Walukiewicz, Igor: Static analysis of deterministic negotiations. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE, 2017 mehr…
  • Fijalkow, Nathanaël; Gimbert, Hugo; Kelmendi, Edon; Kuperberg, Denis: Stamina: Stabilisation Monoids in Automata Theory. In: Implementation and Application of Automata. Springer International Publishing, 2017 mehr…
  • Muscholl, Anca; Seidl, Helmut; Walukiewicz, Igor: Reachability for Dynamic Parametric Processes. In: Lecture Notes in Computer Science. Springer International Publishing, 2017 mehr…

2016

  • Baschenis, Félix; Gauwin, Olivier; Muscholl, Anca; Puppis, Gabriele: Minimizing Resources of Sweeping and Streaming String Transducers. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2016 mehr…
  • Chang, Wanli; Roy, Debayan; Zhang, Licong; Chakraborty, Samarjit: Model-based design of resource-efficient automotive control software. Proceedings of the 35th International Conference on Computer-Aided Design - ICCAD '16, ACM Press, 2016 mehr…
  • Kuperberg, Denis; Brunel, Julien; Chemouil, David: On Finite Domains in First-Order Linear Temporal Logic. In: Automated Technology for Verification and Analysis. Springer International Publishing, 2016 mehr…
  • Macedo, Nuno; Brunel, Julien; Chemouil, David; Cunha, Alcino; Kuperberg, Denis: Lightweight specification and analysis of dynamic systems with rich configurations. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering - FSE 2016, ACM Press, 2016 mehr…
  • Roy, Debayan; Zhang, Licong; Chang, Wanli; Goswami, Dip; Chakraborty, Samarjit: Multi-Objective Co-Optimization of FlexRay-Based Distributed Control Systems. 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), IEEE, 2016 mehr…
  • Yunge, Daniel; Park, Sangyoung; Kindt, Philipp; Pravadelli, Graziano; Chakraborty, Samarjit: Dynamic service synthesis and switching for medical IoT and ambient assisted living. 2016 IEEE International High Level Design Validation and Test Workshop (HLDVT), IEEE, 2016 mehr…

2015

  • Almagor, Shaull; Kuperberg, Denis; Kupferman, Orna: The Sensing Cost of Monitoring and Synthesis. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2015 mehr…
  • Althoff, Daniel; Althoff, Matthias; Scherer, Sebastian: Online safety verification of trajectories for unmanned flight with offline computed robust invariant sets. 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, 2015 mehr…
  • Durand-Gasselin, Antoine; Esparza, Javier; Ganty, Pierre; Majumdar, Rupak: Model Checking Parameterized Asynchronous Shared-Memory Systems. In: Computer Aided Verification. Springer International Publishing, 2015 mehr…
  • La Torre, Salvatore; Muscholl, Anca; Walukiewicz, Igor: Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2015 mehr…
  • Mundhenk, Philipp; Steinhorst, Sebastian; Lukasiewycz, Martin; Fahmy, Suhaib A.; Chakraborty, Samarjit: Security analysis of automotive architectures using probabilistic model checking. Proceedings of the 52nd Annual Design Automation Conference on - DAC '15, Association for Computing Machinery (ACM), 2015 mehr…
  • Mundhenk, Philipp; Steinhorst, Sebastian; Lukasiewycz, Martin; Fahmy, Suhaib A.; Chakraborty, Samarjit: Security analysis of automotive architectures using probabilistic model checking. Proceedings of the 52nd Annual Design Automation Conference on - DAC '15, ACM Press, 2015 mehr…
  • Muscholl, Anca: Automated Synthesis of Distributed Controllers. In: Automata, Languages, and Programming. Springer Berlin Heidelberg, 2015 mehr…
  • Rungger, Matthias; Zamani, Majid: Compositional construction of approximate abstractions. Proceedings of the 18th International Conference on Hybrid Systems Computation and Control - HSCC '15, ACM Press, 2015 mehr…
  • Saha, Ratul; Esparza, Javier; Jha, Sumit Kumar; Mukund, Madhavan; Thiagarajan, P. S.: Distributed Markov Chains. In: Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2015 mehr…
  • Zamani, Majid; Abate, Alessandro; Girard, Antoine: Symbolic models for stochastic switched systems: A discretization and a discretization-free approach. Automatica 55, 2015, 183-196 mehr…