Bettina Könighofer
Dipl.-Ing. BScPhD Students, Team Bloem
Bettina Könighofer is Ph.D. candidate at Graz University of Technology, supervised by Roderick Bloem and a member of the Systematic Construction of Correct Systems group. Before joining IAIK in 2013, she studied Computer Science at Graz University of Technology and completed her graduate studies with distinction. Her research interests lie primarily in the area of reinforcement learning, formal verification and synthesis of hardware and software.
Research
The goal of my Ph.D. is to combine the best of two worlds, namely (1) the formal correctness guarantees of a controller with respect to a temporal logic specification, as provided by formal methods (and reactive synthesis in particular), and (2) the optimality with respect to an a priori unknown performance criterion, as provided by reinforcement learning.
Reinforcement learning algorithms discover policies that maximize reward, but do not guarantee safety during learning or execution phases.
We introduce a new approach to learn optimal policies while enforcing safety properties expressed in temporal logic.
Additionally, our approach has the potential to increase learning efficiency by reducing the number of training episodes by orders of magnitude.
Teaching
Since 2015, I’m lecturing the bachelor course:
- ** Logic and Compatibility** (lecture and practicals: summer term) I teach formal specifications, synthesis and game theory as part of the graduate course:
- ** Selected Topics Design and Verification** (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. Looking for a bachelor’s thesis, master’s thesis, or project in formal methods for AI? Let us know, we’re always happy to discuss open topics!