Formal Verification and Control Synthesis of Complex Dynamical Systems

This talk looks at the development of new techniques, based on sound approximations, to formally verify complex systems (such as Cyber-Physical Systems) and to provide computable approaches for the correct-by-design synthesis of control architectures. The approach employs techniques and concepts from the formal verification area over models and problems from the field of dynamical systems and control theory. 

While emphasising the generality of the approach over a diverse set of model classes, this talk zooms in on general models with two main characteristics: probabilistic dynamics and heterogeneous components (continuous/discrete, i.e. hybrid). Such models are a natural framework for  CPS applications. 

Case studies are employed to clarify concepts and techniques. Theory is complemented by algorithms, all packaged in software tools that are freely available to users.