LTL公式的大小是多少？

Question

就复杂性而言，LTL公式的大小通常表示为| p |原子命题的数量，深度还是别的？

在此先感谢！

Answer 1

就复杂性而言，计算公式中使用的运营商的数量X和U是有意义的。请注意，您可以把运营商如˚F，摹，[R和W¯¯为使用ù（见Syntax of LTL）语法糖。

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

更确切地说，当你使用例如Lichtenstein和Pnueli的算法来验证公式，您可以在大小为< = s * 2^n的图中搜索强连通组件（SCC），其中s是状态数。

如果您的LTL语法允许运营商过去，太，那么你可以添加运营商Ÿ和小号类似。