InOVationCS · Intelligence-Oriented Verification&Controller Synthesis

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 goes one step further and avoids the manual implementation, providing a correct-by-construction controller directly. Despite considerable advances, scalable solutions remain elusive here. 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 challeges since models, properties and controllers are now often based on data rather than design. Due to their “black-box” nature, the resulting systems are (i) even harder to verify, and (ii) not explainable enough to be responsibly deployed. 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. 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. 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