|
所在平台: Coursera |
课程主页: https://www.coursera.org/learn/automated-reasoning-symbolic-model-checking
课程评论：没有评论
课程名称：自动推理：符号模型检测 课程概述：本课程介绍如何自动验证系统和程序的属性。基本概念是转换系统：可以用状态和步骤描述的任何系统。课程中将介绍如何用计算树逻辑（CTL）描述可达性等属性。由于状态空间通常非常大，解决问题的一种方法是符号模型检测：一种用符号表示状态集合的方法。一种有效的表示方式是使用二叉决策图（BDD）。 课程内容包括BDD的定义、基本属性及计算算法，这些内容对于进行CTL模型检测是必需的。 课程大纲： 1. CTL模型检测 - 描述：在MOOC的一般介绍之后，本模块对模型检测进行了概述。随后引入计算树逻辑（CTL），这是一种描述转换系统属性的语言。提供了检验某一属性是否成立的算法，而没有详细说明状态集合的表示方式。 2. BDDs第一部分 - 描述：本模块介绍了BDD（二叉决策图）作为共享的决策树，表示布尔函数。讨论了对决策树和BDD的额外要求，从中可以得出表示的唯一性。 3. BDDs第二部分 - 描述：在展示了一些BDD例子后，提供了计算任何命题公式的ROBDD算法，并进行了讨论。 4. 基于BDD的符号模型检测 - 描述：在最后一个模块中，将CTL模型检测和BDD结合，展示了如何使用BDD以一种方式表示状态集合，从而可以应用CTL模型检测的抽象算法，并且处理比显式状态模型检测更大的状态空间。提供了多个示例。 本课程适合想深入了解自动化推理及符号模型检测的学生和专业人士。
Name:CTL model checking
Description:After a general introduction to the MOOC, this module starts by a general description of model checking.Then Computation Tree Logic (CTL) is introduced: a language in which properties on transition systems can be described. The algorithm to check whether such a property holds is given in an abstract setting, leaving implicit how sets of states are represented.
Name:BDDs part 1
Description:In this module BDDs (binary decision diagrams) are introduced as decision trees with sharing. They represent boolean functions. Extra requirements on both decision trees and BDDs are presented from which uniqueness of the representation can be concluded.
Name:BDDs part 2
Description:After some examples of BDD, the algorithm is presented and discussed to compute the ROBDD of any propositional formula.
Name:BDD based symbolic model checking
Description:In this last module the topics of CTL model checking and BDDs are combined: it is shown how BDDs can be used to represent sets of states in a way that the abstract algorithm for CTL mode checking can be used, and much larger state spaces can be dealt with than by using explicit state based model checking. Sever examples are presented.
This course presents how properties of acting systems and programs can be verified automatically. The basic notion is a transition system: any system that can be described by states and steps. We present how in CTL (computation tree logic) properties like reachability can be described. Typically, a state space may be very large. One way to deal with this is symbolic model checking: a way in which sets of states are represented symbolically. A fruitful way to do so is by representing sets of states by BDDs (binary decision diagrams). Definitions and basic properties of BDDs are presented in this course, and also algorithms to compute them, as they are needed for doing CTL model checking.
