有人可以花几句话向不是来自正式方法背景的人解释一下，当搜索有时间限制时，使用符号模型检查验证规范和使用具体模型检查验证规范有什么区别？我指的是 UPPAAL 中对 SMC 和 Concrete MC 的定义。
特别是，我编写了一个程序，它使用 UPPAAL Java API 来验证针对定时自动机网络的查询。如果查询被验证，UPPAAL 返回一个符号跟踪来解析，如果不是，则返回其他东西。如果验证时间太长，我决定停止验证过程，返回一条消息并继续下一个查询以进行验证。到目前为止一切都很好。
最近，我一直在玩 UPPAAL Stratego，它本机提供了选择最大时间或探索深度来限制搜索的可能性。但是，只有在使用具体模型检查执行验证时才能应用此选项。
我的问题是：停止符号验证过程有什么区别，就像我在我的 Java 程序中所做的那样，以及 UPPAAL Stratego 本身是做什么的？在这两种情况下，我都没有得到答案（或踪迹），但是探索的“可靠性”呢？
这两个选项之间哪个更好（即更完整）？停止符号验证还是停止具体验证？
到目前为止，我的理解是，在符号模型检查中，可能的状态是通过使用变量间隔来定义的，而在具体模型检查中，变量假设一个实际值。我的观点是，就“完整性”而言，在一段时间后停止 SMC 更“完整”，因为状态空间的探索是使用 BFS 或 DFS 算法系统地发生的，如果我使用 BFS，我可以“确定”在 N 步内没有任何不好的事情发生。但同样，我在模型检查方面的背景并不丰富，所以我可能完全搞错了。
此外，如果可以放弃对策略的任何引用，将不胜感激。
谢谢！