Neural Abstraction-Based Controller Synthesis and Deployment
Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani

TL;DR
This paper introduces neural network-based methods to significantly reduce memory requirements in abstraction-based controller synthesis and deployment, maintaining correctness and enabling practical application.
Contribution
It proposes a novel on-the-fly synthesis algorithm and a training method for neural controllers that ensure soundness and drastically cut memory usage.
Findings
Memory reduction factor of up to 7.54×10^5 for synthesis
Memory reduction factor of up to 3.18×10^4 for deployment
Approach maintains correctness despite compression
Abstract
Abstraction-based techniques are an attractive approach for synthesizing correct-by-construction controllers to satisfy high-level temporal requirements. A main bottleneck for successful application of these techniques is the memory requirement, both during controller synthesis and in controller deployment. We propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques using neural network representations. To perform synthesis for reach-avoid specifications, we propose an on-the-fly algorithm that relies on compressed neural network representations of the forward and backward dynamics of the system. In contrast to usual applications of neural representations, our technique maintains soundness of the end-to-end process. To ensure this, we correct the output of the trained neural network such that the corrected output representations are…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdversarial Robustness in Machine Learning · Formal Methods in Verification · Model Reduction and Neural Networks
