model-checking - LTL 公式的大小是多少？

Question

就复杂性而言，LTL 公式的大小 |p| 通常是什么意思？原子命题的数量，深度还是其他？

提前致谢！！

Answer 1

就复杂性而言，计算公式中使用的X和U运算符的数量是有意义的。请注意，您可以将F、G、R和W等运算符视为使用U的语法糖（请参阅LTL 的语法）。

理由：在对系统进行模型检查时，您必须考虑系统每个状态的每个可能的未来。因此，您必须考虑X ... 或 ... U ...形式的子公式可能为真或假。因此，每个状态都有 2^n 种可能性，其中 n 是X和U运算符的数量。

更准确地说，当您使用例如 Lichtenstein 和 Pnueli 的算法来验证公式时，您会在大小 <= s*2^n 的图中搜索强连通分量 (SCC)，其中 s 是状态数。

如果您的 LTL 语法也允许过去的运算符，那么您可以类似地添加运算符Y和S。