Sound, Automated, and scalable, Synthesis of Digital Controllers for Physical Systems

Brief description of the context of the research including potential impact: Connections between verification and control underpin work on the development of symbolic methods and automated techniques based on SAT/SMT theory for the synthesis of CPS.
This project will employ powerful techniques from bounded model checking and inductive synthesis (CEGIS and SyGuS) to automatically design sound digital controllers for physical plants (1,2). The approach allows for the design and synthesis of modern control architectures, implemented over digital devices such as FPGAs using automatic procedures that are correct by construction. The synthesis is sound with respect to the complete range of approximates related to utilising digital architectures for physical plants including: time discretisation, quantisation and saturation effects, and finite-precision arithmetics with rounding errors.

Aims and Objectives: The end-goal of this project is to contribute towards the development of a new, automated, sound and scalable framework, improving industrially relevant state-of-the-art results in digital control systems.
Novelty of the Research Method: Recently (3) has employed the CEGIS architecture to automatically and soundly synthesise Lyapunov control functions for control systems, successfully using neural networks as templates for Lyapunov functions. This project seeks to extend this work to synthesisng controllers of physical systems.


Alignment to EPSRC's strategies and research areas: This project will be in line with EPSRC's research areas in Verification and correctness and control engineering.

(1) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants, CAV17, LNCS 10426, pp 462-482, 2017.
(2) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants, Acta Informatica, In Press, 2020.
(3) D. Ahmed, A. Peruffo and A. Abate, Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers, TACAS20, To Appear, 2020.

AIMS's impact will be felt across domains of acute need within the UK. We expect AIMS to benefit: UK economic performance, through start-up creation; existing UK firms, both through research and addressing skills needs; UK health, by contributing to cancer research, and quality of life, through the delivery of autonomous vehicles; UK public understanding of and policy related to the transformational societal change engendered by autonomous systems.

Autonomous systems are acknowledged by essentially all stakeholders as important to the future UK economy. PwC claim that there is a £232 billion opportunity offered by AI to the UK economy by 2030 (10% of GDP). AIMS has an excellent track record of leadership in spinout creation, and will continue to foster the commercial projects of its students, through the provision of training in IP, licensing and entrepreneurship. With the help of Oxford Science Innovation (investment fund) and Oxford University Innovation (technology transfer office), student projects will be evaluated for commercial potential.

AIMS will also concretely contribute to UK economic competitiveness by meeting the UK's needs for experts in autonomous systems. To meet this need, AIMS will train cohorts with advanced skills that span the breadth of AI, machine learning, robotics, verification and sensor systems. The relevance of the training to the needs of industry will be ensured by the industrial partnerships at the heart of AIMS. These partnerships will also ensure that AIMS will produce research that directly targets UK industrial needs. Our partners span a wide range of UK sectors, including energy, transport, infrastructure, factory automation, finance, health, space and other extreme environments.

The autonomous systems that AIMS will enable also offer the prospect of epochal change in the UK's quality of life and health. As put by former Digital Secretary Matt Hancock, "whether it's improving travel, making banking easier or helping people live longer, AI is already revolutionising our economy and our society." AIMS will help to realise this potential through its delivery of trained experts and targeted research. In particular, two of the four Grand Challenge missions in the UK Industrial Strategy highlight the positive societal impact underpinned by autonomous systems. The "Artificial Intelligence and data" challenge has as its mission to "Use data, Artificial Intelligence and innovation to transform the prevention, early diagnosis and treatment of chronic diseases by 2030". To this mission, AIMS will contribute the outputs of its research pillar on cancer research. The "Future of mobility" challenge highlights the importance the autonomous vehicles will have in making transport "safer, cleaner and better connected." To this challenge, AIMS offers the world-leading research of its robotic systems research pillar.

AIMS will further promote the positive realisation of autonomous technologies through direct influence on policy. The world-leading academics amongst AIMS's supervisory pool are well-connected to policy formation e.g. Prof Osborne serving as a Commissioner on the Independent Commission on the Future of Work. Further, Dr Dan Mawson, Head of the Economy Unit; Economy and Strategic Analysis Team at BEIS will serve as an advisor to AIMS, ensuring bidirectional influence between policy objectives and AIMS research and training.

Broad understanding of autonomous systems is crucial in making a society robust to the transformations they will engender. AIMS will foster such understanding through its provision of opportunities for AIMS students to directly engage with the public. Given the broad societal importance of getting autonomous systems right, AIMS will deliver core training on the ethical, governance, economic and societal implications of autonomous systems.