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

Question

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

提前致谢!

Answer 1

就复杂性而言，计算公式中使用的 X 和 U 运算符的数量是有意义的。请注意，您可以将 F、G、R 和 W 等运算符视为使用 U(参见 Syntax of LTL)。

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

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

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