Coq可以(轻松)用作模型检查器吗? [英] Can Coq be used (easily) as a model checker?
问题描述
正如标题所述，Coq可以用作模型检查器吗?我可以将模型检查与Coq证明相结合吗?这是平常的吗? Google谈论"µ演算"，是否有人对此有类似的经验?建议以这种方式使用Coq，还是我应该寻找其他工具?
类似于 Coq 的证明助手将进行验证您的证明是正确的，并且您提出的任何定理都可以(或不能)使用公理和先前证明的结果来推导.它还将为您提出举证步骤提供支持，以减少您为出示举证而必须付出的努力.
相比之下，模型检查器象征性地枚举了规范的状态空间，并确定是否违反了任何验证条件.在这种情况下，它将提供一条错误跟踪，显示哪些状态更改顺序将触发违规.这些通常具有非常不同的后端处理要求，但是尽管可以将它们组合成一个工具，但Coq证明者似乎并没有这样做.
行为的时空逻辑( TLA +)规范语言，以及随附的 TLA +证明系统( TLAPS)是莱斯利·兰波特(Leslie Lamport)提出的，理由是它涉及大量正式规范.它已经使用 PlusCal 算法语言进行了扩展支持对转换为TLA +表示形式的算法进行模型检查.
µ-calculus 是一种表示法，用作许多形式方法的低级基础.您还应该查看布尔可满足性问题，以寻求更强力的解决方案.定理证明者通常在设计上更加复杂，并使用传统的专家系统/AI概念以及专家定义的证明规则库来提供履行证明义务所需的支持.
作为证明工具的另一个示例，您可以查看 Event-B方法和随附的Rodin开发平台.在完善规范时，这将更具体地确定举证义务并尝试机械地履行这些义务，而让困难的工作留给您去做.
对于模型检查，您可以查看:
在免费提供的选项中.
As the title says, can Coq be used as a model checker? Can I mix model checking with Coq proving? Is this usual? Google talks about a "µ-calculus", does anyone have experience with this or something similar? Is it advised to use Coq in this way, or should I look for another tool?
A proof assistant like Coq will verify that your proof is sound and that any theorems you propose can (or cannot) be derived using axioms and previously proven results. It will also provide you with support in proposing proof steps to reduce the effort you have to make to discharging the proofs.
A model checker, in contrast, symbolically enumerates the state space of the specification and determines whether any of the verification conditions are violated. In such a case, it will provide an error trace showing what sequence of state changes will trigger the violation.
These usually have very different back-end processing requirements but, while they could be combined into a single tool, the Coq prover does not appear to have done so.
The Temporal Logic of Actions (TLA+) specification language, along with the companion TLA+ Proof System (TLAPS) was developed by Leslie Lamport to reason about large formal specifications. It has been extended with the PlusCal algorithmic language that supports model checking of the algorithms that are translated into a TLA+ representation.
The µ-calculus is a notation used as a low-level underpinning for many formal methods approaches. You should also look at the Boolean satisfiability problem for a more brute force approach. Theorem provers are generally more sophisticated in their design and use traditional expert system/AI concepts along with libraries of proof rules defined by experts to provide the support required to discharge the proof obligations.
As an another example of a proof tool, you can look at the Event-B method and the accompanying Rodin development platform. This will, when refining a specification more concretely identify the proof obligations and attempt to mechanically discharge these, leaving the difficult ones for you to do.
For model checking you could look at:
among the freely available choices.
这篇关于Coq可以(轻松)用作模型检查器吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
