Report
Teaser, summary, work performed and final results
Periodic Reporting for period 1 - PROCSYS (Towards programmable cyber-physical systems: a symbolic control approach)
Teaser
\"Autonomous vehicles, intelligent buildings or robots promise to transform the everyday life of our society in all its dimensions (transport, housing, industry, health, assistance to the elderly ...). These systems are examples of cyber-physical systems (CPS) resulting from...
Summary
\"Autonomous vehicles, intelligent buildings or robots promise to transform the everyday life of our society in all its dimensions (transport, housing, industry, health, assistance to the elderly ...). These systems are examples of cyber-physical systems (CPS) resulting from the integration of computer components and physical processes. The development of these systems is often complex (due to cyber-physical interactions) and with critical safety requirements.
The main objective of the PROCSYS project is to provide a framework for CPS programming that allows fast and safe development of their functionality through a high-level programming language. Synthesis algorithms will automatically generate low-level controllers that perform the specified behavior. The originality of the approach is to consider that the program is not intended to be executed on the digital platform made up of computer components (as is traditionally done), but on the cyber-physical platform also including the physical part of the system. Thus, the high-level programs do not specify the behavior of the computer components but directly that of the cyber-physical system. This is a paradigm shift in CPS programming. The knowledge of a model of the physical process is then essential to the synthesis of the low-level controllers.
Cyber-physical systems (CPS) consist of computational elements monitoring and controlling physical entities. The main objective of the PROCSYS project is to propose a general framework for the design of programmable CPS that will allow engineers to develop advanced functionalities using a high-level programming language for specifying the behaviours of a CPS while abstracting the details of the physical dynamics. Controllers enforcing the specified behaviours will be generated from a high-level program using an automated model-based synthesis tool. Correctness of the controllers will be guaranteed by following thecorrect by construction synthesis paradigm through the use of symbolic control techniques: the continuousphysical dynamics is abstracted by a symbolic model, which is a purely discrete dynamical system; aninterface consisting of low-level controllers is designed such that the physical system and the symbolic model behaves identically; a high-level symbolic controller is then synthesized automatically from the high-level program and the symbolic model. We will develop a high-level programming language, based on the intuitive formalism of hybrid automata, which will enable to specify a rich set of behaviours while enabling the development of efficient controller synthesis algorithms. The project will also tackle the two main
bottlenecks in the area of symbolic control, which will enable its use in challenging real-life applications. Firstly, scalability of symbolic control will be achieved by the computation of more compact symbolic models and by controller synthesis algorithms that require only partial exploration of the symbolic models. Secondly, robustness will be ensured at all levels of control by developing novel algorithms for the synthesis of robust interfaces and of symbolic controllers. The algorithms developed in the project will be implemented in a symbolic control toolbox, which will enable the use of our approach by systems engineers.
The programming language developed in the project is directly inspired by the formalism of the hybrid automaton, and will allow, among other things, to describe in a more operational way all the behaviors expressible in linear temporal logic, which is a specification language widely used for CPS. Following the paradigm of \"\"correct by construction synthesis\"\", low-level controllers will be synthesized by symbolic control techniques. The key concept of symbolic control is that of the symbolic model, which is a dynamic finite state system, obtained by abstracting physical trajectories on a finite set of symbols. When symbolic and physical dynamics are formally linked by a behavioral rel\"
Work performed
We are working towards the definition of a high-level language for CPS programming. Control programs defined in this language specify how a set of elementary control tasks should be sequenced. A control task is then specified by a hybrid automaton, which is a popular modeling formalism for CPS. Control tasks can be equipped with to types of semantics specifying if the task must finish in finite time or can last forever. A control program makes it possible to define external inputs, which enable communication with a human user or with other CPS through a digital interface. We have analyzed the expressivity of the proposed programming language. It clearly encompasses hybrid automata but we have proved that it also makes it possible to specify all properties expressed in Linear Temporal Logic, a popular specification formalism for CPS. We have also worked towards the development of algorithms for synthesizing low-level controllers that realize the behavior specified in a control program. We essentially developed two approaches. The first approach focuses on completeness (i.e. we determine the set of all controllable states and synthesize the associated maximal controller) and relies on outer-fixed point computation. This approach can be computationally demanding. The second approach focuses on efficiency and relies on inner-fixed point computation. The synthesis algorithm can be stopped at any time and still provide an admissible controller. However, the approach is in general conservative. We are currently performing numerical case studies in the field of autonomous vehicles.
We have worked on improving the scalability of symbolic control approaches. Firstly, we have developed several approaches for the computation of parsimonious symbolic models, which count a reduced number of symbolic states for a given precision.
Such approaches are based on multi-rate sampling, event-based sampling or singular perturbation approximation methods for systems with multiple time-scales. We are now working on the development of algorithms for the efficient synthesis of controllers. These algorithms (called lazy) only explore partially and incrementally the dynamics of the symbolic model. For safety specifications, we have developed approaches that can apply to multi-scale symbolic models, event based sampling or monotone dynamical systems.
As for robustness of symbolic control, we have worked towards the development of quantitative synthesis algorithms for safety properties. These algorithms synthesize controllers that maximize the level of safety of the system. We are currently working toward the extension of this approach to reachability and stability properties.
The results of the project have been presented in several publications and in several invited plenary or keynote talks in conferences (International Conference on Hybrid Systems: Computation and Control, 2018; European Control Conference, 2018; Journées de l\'Automatique 2018).
Final results
We have proposed a programming language for CPS that encompasses several existing formalisms. Associated controller synthesis algorithms have been developed. We are now working towards applying the proposed language in case studies to evaluate its effectiveness. These case studies will also help us to identify the useful extensions that can be brought to the language. We have developed several approaches to compute parsimonious symbolic models of CPS. We are currently developing efficient synthesis algorithms that explore partially and incrementally there dynamics of the symbolic model. We have focused on specific classes of systems and on safety properties. In the future, we will consider more general classes of systems and extend the approach to other types of properties such as those expressed in our high-level programming language. We have developed a quantitative version of the safety controller synthesis algorithm. We are currently extending this work to reachability and stability properties. In the future, we will also adapt these algorithms for achieving robustness to unmodelled disturbances. We will also develop quantitative synthesis algorithms for our CPS programming language. A symbolic control toolbox, including algorithms developed in the project, will be developed. This toolbox will enable the use of our approach by systems engineers.