Switching Protocols for Formal Composition of Low-level Dynamics in Cyber-physical Systems
Abstract:
An outstanding challenge in the design of reliable cyber-physical systems is the complex interactions between heterogeneous system components as well as interactions with the dynamic environment the system operates in. In this talk, I will present an hierarchical control framework for nonlinear switched systems where the interactions both with the environment and between different layers of the system are abstracted by novel finite-state representations. I will then focus on formal synthesis of reactive switching protocols for switched systems in order to guarantee that the trajectories of the system satisfy certain high-level specifications expressed in linear temporal logic. By exploiting the abstract representations, the synthesis problem can be recast as a two-player temporal-logic game. By construction, existence of a winning strategy for the system in this game guarantees the existence of a continuously implementable switching protocol. I will also discuss recent progress on computing and incrementally refining abstract representations based on counter-examples from a game-solver or due to the changes in the design requirements. I will conclude the talk with some applications in robot motion planning and composition of pre-designed feedback controllers.