Formal methods for the control of Cyber Physical Systems with Logic Specifications

  • Date January 30, 2018
  • Hour 5 pm
  • Room GSSI Main Lecture Hall
  • Speaker Giordano Pola (DISIMI, Università dell'Aquila)
  • Area Computer Science


A challenging paradigm in the design of modern engineered systems are Cyber–Physical Systems (CPS). CPS are complex, heterogeneous, spatially distributed systems where physical processes interact with distributed computing units through non-ideal communication networks. Key features of CPS are heterogeneity and complexity. Indeed, while physical processes are generally described by differential equations, computing units are generally described by finite state machines. To complicate things, communication infrastructures, conveying information in sub–systems of CPS, are characterized by a number of non–idealities that are needed to be considered towards a robust control design of such systems. The paradigm of symbolic models is promising of being appropriate in coping with the inherent heterogeneity of CPS. Symbolic models are abstract descriptions of control systems where any state corresponds to an aggregate of continuous states and any control label to an aggregate of control inputs. Since symbolic models are of the same nature of the mathematical models of the computing units, they offer a sound approach for solving control problems in which software and hardware interact with the physical world, as in the case of CPS. Furthermore by using symbolic models, one can address a wealth of novel logic specifications that are difficult to enforce by means of conventional control design methods. In this talk I will give an overview of my research in this area and show an approach based on symbolic models for the control design of CPS. I will first show how a symbolic model can be constructed which approximates a nonlinear control system with any desired accuracy. I then will show how this symbolic model can be used to design digital and quantized controllers for enforcing complex logic specifications on the original nonlinear system. I will finally briefly discuss how these results can be extended to more realistic scenarios including disturbance inputs, time-delays in the state and control variables evolution, nonideal communication infrastructures, etc. Techniques to tame computational complexity of the approach taken will be also briefly discussed.