Software Tools
Presented below is a collection of the software tools I have created as part of my research. Do check them out!
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems
IMPaCT is an open-source software tool for the parallelised verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage interval iteration algorithms for formal verification and controller synthesis over infinite-horizon properties, including safety, reachability, and reach-while-avoid, while offering convergence guarantees.
PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems
PRoTECT is an open-source software tool for the parallelized construction of safety barrier certificates (BCs) for nonlinear polynomial systems. This tool employs sum-of-squares (SOS) optimization programs to systematically search for polynomial-type BCs, while aiming to verify safety properties over four classes of dynamical systems: (i) discrete-time stochastic systems, (ii) discrete-time deterministic systems, (iii) continuous-time stochastic systems, and (iv) continuous-time deterministic systems.
TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory
TRUST is an open-source software tool developed for data-driven controller synthesis of dynamical systems with unknown mathematical models, ensuring either stability or safety properties. By collecting only a single input-state trajectory from the unknown system and satisfying a rank condition that ensures the system is persistently excited according to the Willems et al.’s fundamental lemma, TRUST aims to design either control Lyapunov functions (CLF) or control barrier certificates (CBC), along with their corresponding stability or safety controllers.