Bettina Könighofer

Research

My main research question is how to proof correctness for systems that are too complex to be formally verified.

We developed a concept for enforcing correctness during runtime. We developed a synthesis approach to automatically construct, from a given safety-critical specification, a SHIELD: a module that monitors the runtime behaviour of a system and interferes if and only if a critical property is violated. Thus, without ever analysing the software program or a reactive hardware, shielding guarantees that the output of the shielded system satisfies the specification.

We applied shields to reinforcement learning agents. For systems employing reinforcement learning, safety of decision-making, particularly during the exploration phase, is a major open challenge. A shield lets a learning agent do whatever it is doing and intervenes with its operation whenever absolutely needed to ensure safety. Thereby, shielding provides formal correctness guarantees for learned controllers, justifying their use in safety critical applications.

The two disciplines, formal methods and machine learning, should benefit from each other’s strengths in any possible way, and the focus of applying formal methods should not only be on guaranteeing safety, but also on ensuring performance. My goal is to further develop our shields such that they can be used by engineers to certificate their systems and can be applied to most demanding and challenging applications such as urban driving automation and intelligent medical devices.

• http://www.onlineshielding.at/
• https://tempest-synthesis.org/