摘要
学习时序逻辑规范从系统示范中提取是进行形式验证和控制器合成的重要任务,尤其是在安全关键领域。现有方法通常假设示范是正确的,或者仅受到误分类错误的影响。然而,在实际应用中,系统轨迹常常由于传感器故障、测量误差或数据丢失而变得不确定或不完整。
我们提出了一种框架,通过不确定性从示范中学习最小线性时序逻辑(LTL)公式。我们的方法通过汉明距离来建模不确定性,以生成围绕每个观察到的轨迹的可能估计,并将这些估计分组,同时要求每组中至少有一个轨迹与学习到的公式一致。我们的任务随后被简化为一个等效的伪布尔优化问题。
我们对我们的方法进行了评估,并与最先进的LTL学习方法进行了比较,结果显示,在不确定性下,我们的方法能够恢复出更接近真实公式的规范。
博主点评: 本文提出了一种新颖的框架来处理不确定性问题,利用汉明距离有效地生成轨迹估计,展现了在安全关键应用中的潜力。该方法的伪布尔优化转换也为未来的研究提供了新的方向,值得关注。