IMPaCT¶

Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems

IMPaCT is an open-source C++ tool for parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov decision processes (IMDPs). Built on AdaptiveCpp (SYCL) for adaptive parallelism across CPUs and GPUs from all hardware vendors.

GPU Accelerated

SYCL-based parallelism via AdaptiveCpp. Runs on CPUs and GPUs from Intel, NVIDIA, and others.

Formal Guarantees

Interval iteration algorithms with convergence guarantees for infinite-horizon specifications.

Flexible Specifications

Safety, reachability, and reach-while-avoid properties over finite and infinite time horizons.

Scalable

Tested from 2D to 14D systems. Parallel construction tackles the state-explosion problem.

Getting Started¶

Installation

Install IMPaCT from source on Linux or macOS, or use Docker.

Installation

Quick Start

Walk through a complete example: define a system, abstract, and synthesize a controller.

Quick Start

Docker

The easiest way to get started — run IMPaCT in a container.

Docker

GPU Setup

Configure GPU acceleration for NVIDIA, Intel, and other hardware.

GPU Setup

Example Case Studies¶

Case Study	Dimensions	Specification	Description
2D Robot	2	Reachability	Mobile robot reaching a target region
2D Robot (Disturbed)	2	Reachability	Robot with additive disturbance
2D Robot Reach-Avoid	2	Reach-Avoid	Reach target while avoiding obstacles
3D Autonomous Vehicle	3	Reach-Avoid	Vehicle navigation with obstacle avoidance
3D Room Temperature	3	Safety	Temperature regulation over finite horizon
4D Building Automation	4	Safety	Multi-room temperature control
7D Building Automation	7	Safety (Verification)	Large-scale IMC verification
14D Stochastic System	14	Safety	High-dimensional scalability demonstration

See all examples ->

API Modules¶

MDP

Base class for state/input/disturbance spaces, dynamics, and noise distributions.

MDP (class MDP)

IMDP

Interval MDP class for abstraction, synthesis, and controller save/load.

IMDP (class IMDP)

GPU Synthesis

Sorted synthesis algorithms optimized for GPU execution via SYCL.

GPU Synthesis

IO Utilities

HDF5 save/load functions for matrices, vectors, and controllers.

IO Utilities (IMPaCT_IO)