Research Areas
Neural Network Safety
Runtime Monitoring of Neural Network
We develop runtime monitors for neural networks to improve their reliability.
Abstraction of Neural Network
We abstract neural networks to improve verification speed.
Automata and Logic
Machine Learning for LTL Synthesis
We apply machine learning to the LTL synthesis problem.
Translating LTL to Automata
We design algorithms for translating LTL to different types of automata.
Explainability
Explaining Controllers via Decision Trees
We develop methods for explaining controllers with decision trees.
Explaining Controllers via Automata
We develop methods for explaining controllers via automata.
Security Analysis via Learning and Model-Checking Attack-Defense Trees
Algorithms for Stochastic Games
Value Iteration for Stochastic Games
We develop value iteration algorithms for stochastic games.
Concurrent Stochastic Games
We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.
