最先进的模型检查器的状态空间大小

Question

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

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

Answer 1

答案千差万别，主要取决于以下因素：

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

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

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

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

• 基于binary-decision diagrams (BDD) 的符号方法的行为方式（几乎）与根据规范可以达到多少状态无关。主要因素是规范的编码中出现了什么样的布尔函数。

  例如，涉及乘数的规范将导致 BDDs that are exponentially large in the number of bits 表示状态，因此大小与状态数量成线性关系（假设可达状态比用于表示这些状态的位数成倍增加） ）。在这种情况下，带有2^50 状态的状态空间可能会被符号分析所禁止。

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

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

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

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

关于术语（上述“规范”），请参阅 Leslie Lamport 的 "What good is temporal logic?"。

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

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

• Bwolen Yang、Randal E. Bryant、David R. O'Hallaron、Armin Biere、Olivier Coudert、Geert Janssen、Rajeev K. Ranjan、Fabio Somenzi，A performance study of BDD-based model checking，FMCAD，1998，DOI：@987654329 @

• Radek Pelánek，Properties of state spaces and their applications，STTT，2008，DOI：10.1007/s10009-008-0070-5（以及相关的website）

• Radek Pelánek，Typical structural properties of state spaces，SPIN，2004，DOI：10.1007/978-3-540-24732-6_2

• Yunja Choi，从 NuSMV 到 SPIN：模型检查飞行引导系统的经验，FMSD，2007，DOI：10.1007/s10703-006-0027-9

• J.R. Burch, E.M. Clarke, K.L.麦克米兰，D.L. Dill, L.J. Hwang, Symbolic model checking: 10^20 states and beyond, LICS, 1990, DOI: 10.1109/LICS.1990.113767