分支时序逻辑的鲁棒空虚性

检测逻辑规约是否被过于容易地满足（即空虚满足）的技术日益受到关注。例如，规约“每个请求最终都会跟随一个确认”被一个从不产生任何请求的系统空虚满足。空虚满足会误导模型检验的用户，使其认为系统是正确的。已有几种关于空虚性的定义。最初，Beer 等人将空虚性形式化为对语法扰动的敏感性。然而，该定义仅对单次出现的空虚性合理。Armoni 等人认为空虚性必须是鲁棒的——不受语义不变变化（例如，用额外的原子命题扩展模型）的影响。他们证明了语法空虚性对 LTL 不是鲁棒的，并提出了一种替代定义——迹空虚性。在本文中，我们继续这一研究方向。我们证明了迹空虚性对分支时序逻辑不是鲁棒的。我们对其进行了改进，使其统一适用于线性时序逻辑和分支时序逻辑，并且不会遭受先前定义中常见缺陷的影响。我们的新定义——互模拟空虚性——是语法空虚性和迹空虚性两者恰当的非平凡扩展。我们讨论了检测互模拟空虚性的复杂性，并为 CTL* 的几个实际相关子集给出了检测空虚性的高效算法。