Probabilistic multi-agent systems
We are working on techniques and tools for verification and strategy synthesis with stochastic games, built into the PRISM-games tool. Recent advances includes methods for concurrent stochastic games and temporal logics and synthesis for equilibria.
Papers: [CAV'20] [QEST'20] [FMSD-21] [TACAS'22] [ARCRAS-22] [MFCS'22] [QEST'23]
Software:
PRISM-games
Verified deep reinforcement learning
We are developing techniques to verify deep reinforcement learning systems, whose controllers are learnt and represented as deep neural networks.
Papers: [FORMATS'20] [IJCAI'21] [NFM'22]
Software:
SafeDRL
Robust verification and control
We are building robust methods for verification and control of stochastic systems in the presence of epistemic uncertainty.
- robust control of continuous-space dynamical systems for unknown noise [AAAI'22, JAIR-23]
- robust anytime learning of MDPs from sampled trajectories [NeurIPS'22]
Software:
PRISM
Verification under partial observation
We are developing techniques for verified probabilistic control unde partial observation, including for:
- model checking POMDPs [RTS-17]
- trust-based planning with POMDPs [ACM-TCPS'22]
- safe POMDP online planning via shielding [ICRA'24]
Software:
PRISM
