论文标题
在信号时间逻辑约束下进行数据驱动的验证
Data-Driven Verification under Signal Temporal Logic Constraints
论文作者
论文摘要
我们考虑在不确定性下的动力学部分未知的系统。我们的目的是通过此类系统的轨迹研究对时间逻辑特性的满意度。我们将这些属性表示为信号时间逻辑公式，并检查满足属性的概率至少是给定阈值。由于动力学是参数化的，并且部分未知，因此我们从系统中收集数据，并采用贝叶斯推理技术将置信值与属性满意度相关联。我们方法的主要新颖性是结合数据驱动和基于模型的技术，以便对系统的行为具有两层概率推理：一层与系统内部的随机噪声有关，下一层与从系统收集的嘈杂数据有关。我们提供近似算法来计算线性动力学系统的置信度。
We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic properties by trajectories of such systems. We express these properties as signal temporal logic formulas and check if the probability of satisfying the property is at least a given threshold. Since the dynamics are parameterized and partially unknown, we collect data from the system and employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system: one layer is related to the stochastic noise inside the system and the next layer is related to the noisy data collected from the system. We provide approximate algorithms for computing the confidence for linear dynamical systems.
