如标题所示，Coq能用作模型检查器吗？我能将模型检查与Coq证明混合使用吗？这种做法常见吗？Google提到了“µ-演算”，有人对此或类似的东西有经验吗？建议以这种方式使用Coq，还是应该寻找其他工具？

我目前正在学习模型检查（模态逻辑、LTL、CTL、SAL模型检查器等），并在业余时间学习Idris，它是一种支持依赖类型的强类型函数式编程语言。由于我同时涉及模型检查和Idris，所以我开始好奇Idris与形式方法和模型检查的关系。 在学习模型检查时，感觉大多数举例都是关于验证用命令式方式编...

符号执行和模型检查有何区别（例如在模型转换中）？我不理解它们之间的区别。它们是一样的吗？

我正在撰写我的硕士论文，需要在时间逻辑中说明和验证我的方法。 在我的情况下，哪种时间逻辑最好使用？我真的希望能得到关于我的方法和如何继续的反馈。 我的模型由参与者组成，将同时执行。对于每个参与者，可以注册规则。它们看起来像这样： conditions -> action 例如。...