Supervisors

Suitable for

Abstract

Prerequisites: Python Programming

Background
Our group has published a series of papers providing a general framework for data-driven abstraction of stochastic dynamical systems [1], [2]. These works introduce methods forconstructing Interval Markov Decision Processes (IMDPs) abstractions directly from data that allows formal verification and synthesis.

Focus
The project focuses on implementing and extending this framework to a scalable tool that uses Python and JAX to enable high-performance parallel computation.

Method
We will:
· Implement the core abstraction framework described in [1], [2] using Python and
JAX.
· Ensure that the implementation supports efficient batching, vectorization, and
parallel computation.
· Evaluate the tool on at least a dozen stochastic dynamical systems

 

Reading:

[1] Nazeri, Mahdi, et al. "Data-Driven Abstraction and Synthesis for Stochastic Systems with Unknown Dynamics." arXiv
preprint arXiv:2508.15543 (2025).
[2] Nazeri, Mahdi, et al. "Data-driven yet formal policy synthesis for stochastic nonlinear dynamical systems." arXiv preprint arXiv:2501.01191 (2025).