IMPaCT: A software tool using IMDPs for control

What is it about?

This work is about the software tool called IMPaCT which uses interval Markov decision processes (IMDPs) to design controllers for dynamical systems affected by stochastic noise. To use the tool, one must provide the system description, including details of the noise, the space in which that system operates, and select one of three types of formal specification; safety, reachability or reach-avoid. The tool will then generate an IMDP that represents the behaviour of that system in the space including the likelihood of transitioning between states. Once the IMDP has been generated, a controller can be designed to enforce the behaviour of the specification selected with some probabilistic confidence. If the user already has the IMDP formulation they can load it into the tool and use the tool simply for the controller design stage.

Featured Image

Photo by Martin Sanchez on Unsplash

Photo by Martin Sanchez on Unsplash

Why is it important?

This tool is important because it provides an efficient service to those looking for controllers that enforce certain behaviours over the system they are analysing. By incorporating parallelism over the CPU and GPU, the tool efficiently generates controllers even for large problems that might require several hundred GB of memory. IMPaCT leverages an algorithm called interval iteration which provides strong guarantees over the convergence to the correct result. This tool is also the only one that can currently design IMDPs for continuous state space systems.

Perspectives