Bettina Könighofer

Dipl.-Ing. BSc

Formal Methods, PhD Candidate

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.
Bettina Könighofer

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 thesismaster’s thesis, or project in formal methods for AI? Let us know, we’re always happy to discuss open topics!

Publications

Shielded Decision-Making in MDPs

Könighofer, B. & Bloem, R.

Safe Reinforcement Learning via Shielding

Bloem, R. & Könighofer, B.
Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, 2669-2678

Shield Synthesis: - Runtime Enforcement for Reactive Systems

Könighofer, B.
Tools and Algorithms for the Construction and Analysis of Systems (TACAS) - 21st International Conference, Springer, 533-548, (Lecture Notes in Computer Science; vol. )

Synthesizing Robust Systems

Könighofer, B.
, 193-220

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

Bloem, R., Iusupov, R., Könighofer, B. & Mangard, S.
EUROCRYPT , Springer, 321-353, (Lecture Notes in Computer Science; vol. )

More Publications