如标题所示，Coq能用作模型检查器吗？我能将模型检查与Coq证明混合使用吗？这种做法常见吗？Google提到了“µ-演算”，有人对此或类似的东西有经验吗？建议以这种方式使用Coq，还是应该寻找其他工具？
3个回答
30
一个像Coq这样的证明辅助工具将验证你的证明是否正确，以及任何你提出的定理是否可以（或不可以）使用公理和已经证明的结果派生。它还将为你提供支持，以提出证明步骤，从而减少你必须进行的证明工作。
相比之下，模型检查器符号枚举规范的状态空间，并确定是否违反任何验证条件。在这种情况下，它将提供一个错误跟踪，显示哪个状态变化序列将触发违规行为。
这些通常具有非常不同的后端处理要求，但是，虽然它们可以合并成一个单一的工具，但Coq证明器似乎没有这样做。
对于模型检查，你可以看看: 其中包括一些免费选择。
相比之下，模型检查器符号枚举规范的状态空间，并确定是否违反任何验证条件。在这种情况下，它将提供一个错误跟踪，显示哪个状态变化序列将触发违规行为。
这些通常具有非常不同的后端处理要求，但是，虽然它们可以合并成一个单一的工具，但Coq证明器似乎没有这样做。
行动的时间逻辑（TLA+）规范语言，以及伴随的TLA+证明系统（TLAPS），是由Leslie Lamport开发的用于推理大型形式化规范的工具。它已经通过PlusCal算法语言进行了扩展，支持将转换为TLA+表示的算法进行模型检查。
μ-演算是许多形式化方法方法的底层基础符号。您还应该查看布尔可满足性问题以获取更加暴力的方法。定理证明器通常在设计上更为复杂，并使用传统的专家系统/人工智能概念以及由专家定义的证明规则库来提供所需的支持以满足证明义务。
作为一个证明工具的另一个例子，你可以看看Event-B方法和相应的Rodin开发平台。当更具体地细化规范时，它将识别证明义务并尝试机械地解决这些问题，留下困难的问题供您解决。对于模型检查，你可以看看: 其中包括一些免费选择。
- Pekka
6
为了补充@Pekka现有的答案，μ-calculus是一种标记用于探讨固定点，这些固定点代表可达性问题的解决方案。
最小不动点（μ）的例子是可以从某个地方到达的最大状态集合（例如，从程序的第一行开始）。它是一个“最少”的不动点，因为它在可能的其他不动点中最小。通过从空集开始，并添加状态直到达到不动点来获得它。在特定条件下，Knaster-Tarski定理保证了不动点的存在。
最大不动点（ν）的例子是我们可以在其中不违反某些安全要求而保留的最大集合。它是一个“最大”不动点，因为它是通过从所有状态的集合开始（因此，在由子集关系定义的部分排序中从上面开始），并逐步限制它，直到达到不动点来获得的。最大不动点对应于最小不动点，因此相同的定理适用于存在和唯一性。将图搜索视为另一个示例。
通过在μ-演算公式中交替使用固定点类型，我们可以表达时间行为，例如：“我希望你不断在两个位置之间来回移动”，或者“我希望服务器最终对收到的每个请求都做出响应”。然后，我们可以使用枚举模型检查器或符号模型检查器进行模型检查，以确定我们所描述的属性是否被我们设计的系统所涵盖。
验证和合成之间的区别在于量词的交替：
主要的实际区别在于，综合和验证是如何使用检查公式是否为真的结果的：
- 在验证中，我们已经拥有了想要的系统的实现，并检查它是否满足某些期望的属性。如果不满足，我们将手动尝试修复实现，然后再次检查。 - 在综合中，一些最终系统的部分我们还没有完全详细说明。我们让工具选择这些细节。换句话说，该工具消除存在量词以使公式为真，并告诉我们它所做的，以便我们将通过这种方式完成系统，确保公式为真。
C语言中综合工具的一个例子是
无论你如何处理问题，至少确保你写下计划，写下规范。这些主题上最好的书之一是Leslie Lamport的“系统规范”。如果想要证明各种表示都是同一事物的不同方面，请阅读“计算机科学与状态机”。
最小不动点（μ）的例子是可以从某个地方到达的最大状态集合（例如，从程序的第一行开始）。它是一个“最少”的不动点，因为它在可能的其他不动点中最小。通过从空集开始，并添加状态直到达到不动点来获得它。在特定条件下，Knaster-Tarski定理保证了不动点的存在。
最大不动点（ν）的例子是我们可以在其中不违反某些安全要求而保留的最大集合。它是一个“最大”不动点，因为它是通过从所有状态的集合开始（因此，在由子集关系定义的部分排序中从上面开始），并逐步限制它，直到达到不动点来获得的。最大不动点对应于最小不动点，因此相同的定理适用于存在和唯一性。将图搜索视为另一个示例。
通过在μ-演算公式中交替使用固定点类型，我们可以表达时间行为，例如：“我希望你不断在两个位置之间来回移动”，或者“我希望服务器最终对收到的每个请求都做出响应”。然后，我们可以使用枚举模型检查器或符号模型检查器进行模型检查，以确定我们所描述的属性是否被我们设计的系统所涵盖。
SPIN是一个枚举模型检查器：它将探索的每个状态存储在哈希表中，并包括一些算法，用于识别它不需要枚举所有状态，而是可以将其中一些状态视为代表其他状态（从验证的属性的角度来看，这些状态是等价的，因此只需要对其中一个进行推理）。这些方法称为部分顺序约简。
NuSMV是一种符号模型检查器。它仍然搜索系统的状态，但不会逐个在内存中表示它们。相反，它跟踪状态的集合，将这些集合表示为二元决策图。这些数据结构可以保持较小的大小，即使它们表示具有
10**24个状态的集合。然而，不能保证这一点。不幸的是，它们仍然可能会增长到很大的尺寸，而几乎所有布尔函数（因此，我们可能想要表示的几乎所有集合）都是如此，正如Claude Shannon已经证明的那样。
验证和合成之间的区别在于量词的交替：
- 验证具有统一的量化（通常是全称量化）
- 合成具有交替的量化：它涉及嵌套的存在量词和全称量词。
\forall x:\exists y:f(x,y)。这难道不就是验证吗？好吧，确实如此，证明了在合成和验证之间，本质上没有任何数学上的区别。传统上，人们主要遇到上述量词出现方式的问题，将其视为合成或验证的问题。主要的实际区别在于，综合和验证是如何使用检查公式是否为真的结果的：
- 在验证中，我们已经拥有了想要的系统的实现，并检查它是否满足某些期望的属性。如果不满足，我们将手动尝试修复实现，然后再次检查。 - 在综合中，一些最终系统的部分我们还没有完全详细说明。我们让工具选择这些细节。换句话说，该工具消除存在量词以使公式为真，并告诉我们它所做的，以便我们将通过这种方式完成系统，确保公式为真。
C语言中综合工具的一个例子是
gr1c，Python中的另一个例子是omega。还有其他工具。无论你如何处理问题，至少确保你写下计划，写下规范。这些主题上最好的书之一是Leslie Lamport的“系统规范”。如果想要证明各种表示都是同一事物的不同方面，请阅读“计算机科学与状态机”。
- 0 _
0
有关使用 Coq 作为模型检查器的一些工作，例如请参见 https://github.com/coq-contribs/smc。但是，我不知道有没有人在重要应用中使用过它。
- Freek Wiedijk
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接