We are developing techniques and software to formally verify AI-based systems, building upon the PRISM toolset.

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

Verified planning under uncertainty
... ...

We are developing a variety techniques for verified planning under uncertainty, including for:

  • planning with mobile robots [IJRR-19]
  • uncertain user preferences [ICCPS'22]
  • distributional probabilistic model checking [NFM'24]

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

Verified neuro-symbolic controllers

We are building approaches for formal modelling and verification of neuro-symbolic agents operating concurrently within a shared, continuous-state environment.

Papers: [UAI'22] [L4DC'24]

This work has been part funded by the projects: FUN2MODEL, PRINCESS