Neural Abstraction-Based Controller Synthesis and Deployment
Neural Abstraction-Based Controller Synthesis and Deployment
复制标题
DOI：
10.1145/3608104
复制
发表时间：
2023-10-01
影响因子：
2
通讯作者：
Soudjani，Sadegh
中科院分区：
文献类型：
--
作者：
Majumdar，Rupak;Salamati，Mahmoud;Soudjani，Sadegh
基于抽象的技术是一种有吸引力的方法，合成正确的建设控制器，以满足高层次的时间要求。这些技术的成功应用的主要瓶颈是内存需求，无论是在控制器合成（存储抽象的转换关系）和控制器部署（存储控制映射）。我们提出了内存有效的方法，用于减轻高内存需求的抽象为基础的技术usingneural network representations。为了进行合成达到避免规范，我们提出了一个在飞行中的算法，依赖于压缩的神经网络表示的系统的前向和后向动态。与神经表征的通常应用相反，我们的技术保持了端到端过程的可靠性。为了确保这一点，我们校正训练后的神经网络的输出，使得校正后的输出表示相对于有限抽象是合理的。对于部署，我们提供了一种新的训练算法，找到一个神经网络表示的合成控制器和实验表明，控制器可以正确地表示为一个神经网络和一个查找表，需要一个小得多的memory.We实验证明，我们的方法显着降低了基于抽象的方法的内存需求的组合。我们比较了我们的方法与标准的基于抽象的合成几个模型的性能。对于所选的基准测试，我们的方法将综合和部署的内存需求分别平均降低了1.31× 105和7.13× 103，最高可达7.54× 105和3.18× 104。虽然这种减少是以增加离线计算来训练神经网络为代价的，但我们方法的所有步骤都是可并行的，并且可以在具有更多处理单元的机器上实现，以减少所需的计算时间。
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 (to store the abstract transition relation) and in controller deployment (to store the control map).We propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques usingneural 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 sound with respect to the finite abstraction. For deployment, we provide a novel training algorithm to find a neural network representation of the synthesized controller and experimentally show that the controller can be correctly represented as a combination of a neural network and a look-up table that requires a substantially smaller memory.We demonstrate experimentally that our approach significantly reduces the memory requirements of abstraction-based methods. We compare the performance of our approach with the standard abstraction-based synthesis on several models. For the selected benchmarks, our approach reduces the memory requirements respectively for the synthesis and deployment by a factor of 1.31× 105and 7.13× 103on average, and up to 7.54× 105and 3.18× 104. Although this reduction is at the cost of increased off-line computations to train the neural networks, all the steps of our approach are parallelizable and can be implemented on machines with higher number of processing units to reduce the required computational time.