Risk of Stochastic Systems for Temporal Logic Specifications
Risk of Stochastic Systems for Temporal Logic Specifications
复制标题
DOI：
10.1145/3580490
复制
发表时间：
2022-05
影响因子：
2
通讯作者：
Lars Lindemann;Lejun Jiang;N. Matni;George Pappas
中科院分区：
文献类型：
--
作者：
Lars Lindemann;Lejun Jiang;N. Matni;George Pappas
数据的广泛可用性，加上人工智能和机器学习的计算进步，有望实现许多未来技术，如自动驾驶。虽然这些技术已经有了各种成功的示范，但多次报告了关键的系统故障。即使这种系统故障很少见，但如果没有严格的风险评估，这种系统故障也会对采用构成严重障碍。本文提出了一个系统和严格的系统风险验证的框架。我们认为制定信号时序逻辑（STL）的系统规范和模型的系统作为一个随机过程，允许离散时间和连续时间的随机过程。然后，我们将STL鲁棒性风险定义为缺乏鲁棒性的风险。这个定义的动机是因为系统故障往往是由于缺乏鲁棒性的建模误差，系统干扰，并在底层数据生成过程中的分布变化。在定义中，我们允许一般类别的风险度量，并专注于尾部风险度量，如风险价值和条件风险价值。虽然STL鲁棒性风险一般难以计算，但我们提出了近似的STL鲁棒性风险作为一个更易于处理的概念，该概念将STL鲁棒性风险上限化。我们展示了如何从系统轨迹数据中准确估计近似STL鲁棒性风险。对于离散时间随机过程，我们证明了在何种条件下近似STL鲁棒性风险甚至可以精确计算。我们说明了我们的验证算法在自动驾驶模拟器CARLA和显示如何风险最小的控制器可以选择四个神经网络车道保持控制器的五个有意义的系统规范。
The wide availability of data coupled with the computational advances in artificial intelligence and machine learning promise to enable many future technologies such as autonomous driving. While there has been a variety of successful demonstrations of these technologies, critical system failures have repeatedly been reported. Even if rare, such system failures pose a serious barrier to adoption without a rigorous risk assessment. This article presents a framework for the systematic and rigorous risk verification of systems. We consider a wide range of system specifications formulated in signal temporal logic (STL) and model the system as a stochastic process, permitting discrete-time and continuous-time stochastic processes. We then define the STL robustness risk as the risk of lacking robustness against failure. This definition is motivated as system failures are often caused by missing robustness to modeling errors, system disturbances, and distribution shifts in the underlying data generating process. Within the definition, we permit general classes of risk measures and focus on tail risk measures such as the value-at-risk and the conditional value-at-risk. While the STL robustness risk is in general hard to compute, we propose the approximate STL robustness risk as a more tractable notion that upper bounds the STL robustness risk. We show how the approximate STL robustness risk can accurately be estimated from system trajectory data. For discrete-time stochastic processes, we show under which conditions the approximate STL robustness risk can even be computed exactly. We illustrate our verification algorithm in the autonomous driving simulator CARLA and show how a least risky controller can be selected among four neural network lane-keeping controllers for five meaningful system specifications.