信息物理系统时序逻辑证伪的局部下降法（扩展技术报告）

分析信息物理系统的一种方式是将其建模为混合自动机。由于混合非线性自动机的可达性分析是非常具有挑战性且计算代价高昂的问题，在实践中，工程师试图解决需求证伪问题。在一种方法中，证伪问题通过最小化由需求诱导的鲁棒性度量来求解。该优化问题通常是非凸非光滑问题，需要启发式与分析性引导才能求解。本文中，混合系统的泛函梯度下降被用于局部减小鲁棒性度量。该局部下降法与模拟退火作为全局优化方法相结合以搜索不安全行为。