Intelligence-Oriented Verification&Controller Synthesis

Introduction

Software making decisions or controlling cyber-physical systems is ubiquitous, hence its correctness is of paramount importance. While the increasing complexity makes manual implementation extremely error-prone, verification can provide formal guarantees on correctness. Verification of hardware and software has seen many successes and industrialization, making systems safe and reliable and their development more efficient.

Controller Synthesis

Controller synthesis goes one step further and avoids the manual implementation, providing a correct-by-construction controller directly. Despite considerable advances, scalable solutions remain elusive here.

Challenges of AI/ML

Artificial intelligence and machine learning (AI/ML) provide scalable solutions to decision making, but at the cost of their reliability, making their verification even more pressing. Besides, the use of AI/ML gives rise to fundamentally new challenges since models, properties, and controllers are now often based on data rather than design.

Black-Box Nature

Due to their “black-box” nature, the resulting systems are:

1. Even harder to verify.
2. Not explainable enough to be responsibly deployed.

Objectives of InOVation&CS

The PI has been pioneering the use of learning in verification to bring together the best of both worlds, scalability and reliability. The main objective of InOVation&CS is to utilize the power of learning in verification and controller synthesis to overcome both the traditional scalability challenges as well as the recent, data-driven ones.

Paradigm Shift

The key to bringing the two closer than ever is a paradigm shift towards explainability and utilizing structure stemming from the presence of intelligence (human or artificial) in the definition, analysis, and solution of real problems, thus providing more information to the learning parts.

Methodology

InOVation&CS shall provide new, more applicable, and more scalable methodology for producing guaranteed reliable controllers.

Keywords

verification, model checking, Markov decision processes, stochastic games, temporal logics