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.
Tools, tutorials and surveys:
[CAV'20]
[ARCRAS-22]
[QEST'23]
[MFCS'22]
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 learning of MDPs from sampled trajectories [NeurIPS'22] [TACAS'25]
Software:
PRISM
Verified planning under uncertainty
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] [RA-L'25]
Software:
PRISM
