Control of Cyber-Physical Systems: a Formal Method approach

Over the past few decades, the rapid evolution of computing has brought to the born of more complex and detailed paradigms of system, named Cyber-Physical Systems (CPS), i.e. systems where physical processes, generally described by continuous dynamics, interact with computing units, generally described by (discrete) models of computation, using a (nonideal) communication infrastructure. The generality of CPS to achieve different and complex scenarios translates in a difficulty to provide systematic methods to their analysis and control. A promising solution is given by hybrid systems, that are dynamical models that combine behaviours of purely continuous dynamics with discrete dynamics. The rich and complex behaviour of such models poses difficulties about how to approach the design of control systems. In the last twenty years, researchers working in the area of computer science and control theory have explored formal methods as an automatic tool for addressing analysis and control design of this complex kind of systems. Central to this approach is the construction of symbolic system that approximate purely continuous or hybrid plants and preserve the same properties of the Cyber-Physical Systems while hiding the details that are of no interest. A symbolic system is an abstract description of a purely continuous or hybrid system where each state corresponds to an aggregate of continuous/hybrid states and each label to an aggregate of continuous/hybrid inputs. The relevance of this approach is corroborated by considering complex logic specifications and mathematical models that can directly incorporate constraints on hardware and software architectures. The contribution of this thesis is to enhance the amount of possible scenario accounted by symbolic systems.