论文标题
椭圆形采样，用于对具有信号时间逻辑规格的随机系统的概率验证
Elliptical Slice Sampling for Probabilistic Verification of Stochastic Systems with Signal Temporal Logic Specifications
论文作者
论文摘要
自主机器人通常将复杂的传感器纳入其决策和控制循环中。这些传感器，例如相机和激光镜头，在感应中存在不完美，并且受环境条件的影响。在本文中，我们提出了一种使用高斯和高斯混合物噪声模型（例如，来自感知模块，机器学习组件）对可线化系统进行概率验证的方法。我们使用Markov Chain Monte-Carlo Slice采样器计算信号时间逻辑（STL）规范下任务满意度的概率。与其他技术相反，我们的方法避免了过度评估和对故障事件的双重计数。我们方法的核心是一种从高斯分布中有效且无排斥的信号采样的方法，从而满足或违反给定的STL公式。我们从机器人运动计划中的应用中显示了说明性示例。
Autonomous robots typically incorporate complex sensors in their decision-making and control loops. These sensors, such as cameras and Lidars, have imperfections in their sensing and are influenced by environmental conditions. In this paper, we present a method for probabilistic verification of linearizable systems with Gaussian and Gaussian mixture noise models (e.g. from perception modules, machine learning components). We compute the probabilities of task satisfaction under Signal Temporal Logic (STL) specifications, using its robustness semantics, with a Markov Chain Monte-Carlo slice sampler. As opposed to other techniques, our method avoids over-approximations and double-counting of failure events. Central to our approach is a method for efficient and rejection-free sampling of signals from a Gaussian distribution such that satisfy or violate a given STL formula. We show illustrative examples from applications in robot motion planning.
