formal-verification - UPPAAL 中的状态空间爆炸

Question

我在 UPPAAL 中模拟了两个触发器的定时模型，当我尝试验证一些属性时，我达到了 6M 状态并且我的笔记本电脑内存不足，消耗了大约 5Go，谁能告诉它是 UPPAAL 可以的近似状态数处理 ？以及在 UPPAAL 中处理状态爆炸的可能技术是什么？
谢谢

Answer 1

状态的数量取决于：

1. 可用内存的大小。在 32 位架构上，它限制为 4GB。

2. 各个州的大小/足迹。

3. 状态空间的形状和探索的顺序。

4. 符号状态的粒度（约束间隔的跨度如何：如果时间离散化，则符号技术的扩展性会很差）。

您可以尝试以下技术：

1. 应用抽象并删除不必要的变量：将变量设为 const，在未使用时将变量设置为零，仅一次转换通信的变量可以标记为“元”（不要滥用这个！否则你会遇到奇怪的行为） .

2. 通过将状态空间缩减设置为积极优化空间消耗。

3. 应用偏序约简，对称约简。

4. 应用扫描线法（在 Uppaal 帮助中查找关键字“progress”）。

查看 Uppaal 教程以获取更多信息。