UPPAAL中的状态空间爆炸

Question

我在UPPAAL中建立了一个两个触发器的定时模型，当我试图验证一些属性时，我达到了6M个状态，我的笔记本电脑没有RAM了，大约5Go被消耗了，有人能告诉我UPPAAL可以处理的大概状态数是多少吗？在UPPAAL中有哪些可能的技术来处理状态爆炸？

谢谢

Answer 1

状态数取决于：

1. 可用内存的大小。在32位架构上，它被限制为4 4GB。
2. 单个状态的大小/占用空间。
3. 状态空间的形状和符号状态的顺序(约束间隔跨度有多好:如果时间是离散化的，则符号技术的伸缩性将很差)。

您可以尝试以下技术：

1. 应用抽象并删除不必要的变量:使变量常量，在不使用时将变量设置为零，只有一次转换通信的变量可以标记为"meta“(不要滥用这一点！)或者，通过将状态空间缩减设置为进度偏序缩减、对称进度扫描线方法(在向上帮助中查找关键字“behavior).
2. optimize”)，您将遇到奇怪的进度空间消耗问题。

有关更多信息，请参阅Uppaal教程。