NExG:基于灵敏度近似的神经网络控制系统可证明引导式状态空间探索

我们提出一种对带有神经网络反馈控制器的闭环控制系统执行状态空间探索的新技术。我们的方法涉及近似闭环动力学轨迹的灵敏度。利用此类近似器和系统模拟器,我们提出了一种引导式状态空间探索方法,可生成在指定时间访问目标状态邻域的轨迹。我们提出一个理论框架,确立我们的方法将产生一系列到达目标状态合适邻域的轨迹。我们在具有不同配置的神经网络反馈控制器的各种系统上对我们的方法进行了全面评估。我们优于先前的状态空间探索技术,并在质量(可解释性)和性能(收敛率)方面取得显著改进。最后,我们采用我们的算法对一类时序逻辑规范进行证伪,评估其相对于最先进证伪工具的性能,并展示其在补充现有证伪算法方面的潜力。