A verified model checker for the modal μ-calculus in Coq
A verified model checker for the modal μ-calculus in Coq
复制标题
DOI：
10.1007/bfb0054171
复制
发表时间：
1998-01-01
期刊：
影响因子：
--
通讯作者：
Sprenger, C
中科院分区：
文献类型：
--
作者：
Sprenger, C
我们报告的形式化和正确性证明的模型检查器的模态μ演算Cog的建设性类型理论。使用Cog的提取机制，我们得到一个可执行的Caml程序，这是作为一个安全的决策过程添加到系统中。因此，我们避免了大的证明对象的生成，同时保持了证明环境的高可靠性。一个例子说明了模型检测与演绎技术的结合。
We report on the formalisation and correctness proof of a model checker for the modal mu-calculus in Cog's constructive type theory. Using Cog's extraction mechanism we obtain an executable Caml program, which is added as a safe decision procedure to the system. We thereby avoid the generation of large proof objects while preserving the high reliability of the proof environment. An example illustrates the combination of model checking with deductive techniques.