The problem of synthesizing controllers for different classes of non-linear systems with respect to temporal logic specifications has received considerable attention in the last decades, especially in the context of cyber-physical system (CPS) design. The goal of these methods is to allow for fully automated synthesis of feedback controllers, which enforce temporal logic constraints and hence, to allow for a much larger spectrum of specifications than classical feedback controller synthesis techniques. In order to achieve this goal, techniques from the formal methods and the control communities need to be combined.
While there has been enormous progress towards this goal in the last decade, most of the existing approaches still tackle the overall problem mainly from either the control or the formal methods side. Thereby, the potential of techniques available in the respective other domain is not fully exploited, leading to unsatisfying solutions in settings where low-layer continuous control and high-layer logical decision making are tightly intertwined.
This line of work investigates a novel approach to such integrated control problems, which automatically computes a provably correct hybrid controller that seamlessly reacts to (high-layer) logical context switches and low-level uncertainties. In particular, we avoid classical brute-force time- and space-discretization for scalability. Instead, we present a novel two-layer strategy synthesis approach, where the controller generated in the lower layer provides invariant sets and basins of attraction, which are exploited at the upper logical layer in an abstract way. In order to achieve this, we provide new techniques for both the upper- and lower-level synthesis.
Our new methodology allows to leverage both the computing power of state space control techniques and the intelligence of finite game solving for complex specifications, in a scalable way.
Group Members Involved:
Former Group Members Involved:
External Collaborators:
- Raphael Jungers (UC Louvain, Belgium)
- Matteo Della Rossa (UC Louvain, Belgium)
- Lucas Neves Egidio
Publications:
- A. Nejati, S. P. Nayak and A.-K. Schmuck. Context-triggered Games for Reactive Synthesis over Stochastic Systems via Control Barrier Certificates. 2024. HSCC’24 (PDF)
- S. P. Nayak, L. N. Egidio, M. Della Rossa, A.-K. Schmuck, R. M. Jungers. Context-Triggered Abstraction-Based Control Design. 2023. IEEE Open Journal of Control Systems. (PDF, HSCC poster)