0

现代模型检查器（如NuSMV）的近似最大状态空间大小是多少。我不需要一个确切的数字，而是一些状态大小值，运行时间仍然可以接受（比如几周）。

除了符号模型检查之外，还有哪些改进用于提高该限制？

4

1 回答 1

2

答案千差万别，除其他因素外，取决于：

  • 使用什么模型检查算法
  • 系统是如何表示的
  • 模型检查器（或其他工具）是如何实现的
  • 软件在什么硬件上运行（以及并行化等）。

我不会提及一些特定的状态，而是会注意一些相关因素（我在下面使用“规范”作为“模型”的同义词）：

  • 符号或枚举：符号算法与枚举算法不同。此外，对于相同的问题，已知的符号和枚举算法的计算复杂度通常存在差异。

  • 枚举在行为上是相对可预测的，因为与具有状态的状态空间N相比，具有状态的状态空间很可能需要更短的时间来枚举1000000 * N。

  • 基于二元决策图(BDD) 的符号方法的行为方式（几乎）与基于规范可达到的状态数量无关。主要因素是规范的编码中出现了什么样的布尔函数。

    例如，涉及乘数的规范将导致BDD 在表示状态的位数上呈指数级增长，因此大小与状态数呈线性关系（假设可达状态比使用的位数呈指数级多）代表这些州）。2^50在这种情况下，具有可能以其他方式进行符号分析的状态的状态空间变得令人望而却步。

    换句话说，重要的不仅是状态的数量，还有系统动作对应的布尔函数的类型（TLA+ 中的动作对应于其他形式中的转移关系）。此外，选择不同的编码（整数位）可能会对 BDD 大小产生影响。

  • 对称性（例如，部分降阶）和抽象是处理更复杂系统分析的一些改进。

  • 可接受的运行时间是一个相对概念。无论采用何种模型检查方法，模型的保真度达到可用时间总是有限制的。

另一种方法是编写具有未指定参数的规范，然后使用模型检查器查找规范实例中与小参数值相对应的错误，并在更正这些错误后，然后使用定理证明器来确保规范的正确性。这种方法得到了TLA+工具的支持，即模型检查器TLC和定理证明器TLAPS。

关于术语（上面的“规范”），请参阅“时间逻辑有什么用？” 通过莱斯利兰波特。

还值得注意的是，根据方法，状态数和可达状态数可能是不同的概念。通常，这在类型化形式中很重要：我们可以指定一个具有 1 个可达状态的系统，但声明导致更多状态的变量类型，其中大多数状态在初始条件下是不可达的。在符号方法中，这会影响编码，从而影响 BDD 的大小。

与状态空间大小相关的参考：

于 2018-01-02T00:34:49.170 回答