Bettina KönighoferDipl.-Ing. Dr.techn. BSc
Formal Methods, Trusted AI
Bettina Könighofer holds a PhD degree in Computer Science from Graz University of Technology. Bettina's research interests lie primarily in the area of reinforcement learning, formal verification, model checking, and synthesis of hardware and software.Office room: IF020680 TUGRAZOnline_Visitenkarte
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.
See example projects:
Since 2015, I’m lecturing the bachelor course:
- Logic and Compatibility (lecture and practicals: summer term)
I teach formal specifications, temporal logic, synthesis and game theory as part of the graduate course:
- Model Checking (lecture and practicals: winter term)
I assisted in several courses in the field of testing, verification and synthesis, and I have co-supervised several Bachelor and Master students.
Könighofer B., Bloem R., Jansen N., Lorber F.
Leveraging Applications of Formal Methods, Verification and Validation, Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings, 2020 International Symposium on Leveraging Applications of Formal Methods, 290-306, (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12476 LNCS)
Jansen N., Könighofer B., Junges S., Serban A., Bloem R.
31st International Conference on Concurrency Theory, CONCUR 2020, 31st CONCUR 2020: Vienna, Austria (Virtual Conference), 31st International Conference on Concurrency Theory, 31-316