课程主页: https://www.coursera.org/learn/automated-reasoning-symbolic-model-checking
在现代计算机科学中，系统的验证尤为重要。Coursera上推出的《自动推理：符号模型检查》课程正是围绕这一主题展开，为学生提供了全面的学习体验。
课程概述
本课程探讨了如何自动验证系统和程序的性质。核心概念是过渡系统：任何可以由状态和步骤描述的系统。课程通过计算树逻辑（CTL）介绍了如何描述可达性等属性。
通常，状态空间可能非常庞大。课程中提出了符号模型检查的概念，这是一种将状态集以符号的方式表示以应对状态空间庞大的问题。
课程大纲
- CTL模型检查
本模块对模型检查进行了概述，介绍了计算树逻辑（CTL），这一语言用于描述过渡系统的性质。还给出了验证属性是否成立的算法。 - BDD部分1
在这部分中，介绍了二进制决策图（BDDs）作为一种共享的决策树，表示布尔函数。强调了对决策树和BDDs的额外要求。 - BDD部分2
在示例后，讲解了计算任意命题公式的ROBDD的算法。 - 基于BDD的符号模型检查
最后一模块结合了CTL模型检查和BDDs，展示了如何使用BDDs表示状态集，从而允许处理比显式状态模型检查更大的状态空间。
这个课程不仅提供了理论知识，还通过具体实例加深了理解。学习者能在实践中掌握符号模型检查技术，这对于系统验证而言至关重要。
因此，我强烈推荐这个课程给所有有志于系统验证的学生和研究人员。
课程主页: https://www.coursera.org/learn/automated-reasoning-symbolic-model-checking