|
所在平台: Coursera |
课程主页: https://www.coursera.org/learn/quantitative-model-checking
课程评论：没有评论
课程名称：量化模型检测 概述：信息与通信技术（ICT）在嵌入式系统、网络物理系统、通信协议和运输系统等应用中的集成迅速增加。因此，这些系统的可靠性和依赖性愈发依赖于软件。缺陷可能是致命的，并且代价高昂（特别是在大规模生产和安全关键系统中）。最初，需要构建一个真实系统的模型。在最简单的情况下，模型反映系统可以达到的所有可能状态及状态之间的所有可能转移，形成一个（标记的）状态转移系统。通过向模型添加概率和离散时间，我们处理所谓的离散时间马尔可夫链，并可进一步扩展到连续时间马尔可夫链。这两种形式在建模、性能和可靠性评估计算机和通信系统中得到了广泛应用。这些形式在数学上具有吸引力，同时又足够灵活以模型复杂系统。 模型检测专注于模型的定性评估。作为一种形式验证方法，模型检测分析系统模型的功能。需要分析的属性必须在具有一致语法和语义的逻辑中进行指定。然后，检查模型的每个状态是否满足该属性。 本课程的主要重点是关于马尔可夫链的量化模型检测，我们将讨论高效的计算算法。本课程的学习目标包括： - 表达不同类型转换系统的依赖性属性。 - 计算马尔可夫链随时间的演变。 - 检查特定公式是否在单个状态下成立，并计算属性的满足集。 课程大纲： 1. 模块1：计算树逻辑 - 描述：介绍带标记转换系统（LTS），计算树逻辑（CTL）的语法和语义，并讨论计算特定CTL公式满足集所需的模型检测算法。 2. 模块2：离散时间马尔可夫链 - 描述：通过引入离散时间，并为转移添加概率以建模概率选择，增强转换系统。讨论DTMC的重要属性，如无记忆性和时间齐次性。状态分类可用于确定极限分布和/或平稳分布的存在性。 3. 模块3：概率计算树逻辑 - 描述：讨论概率计算树逻辑的语法和语义，并检查决定各种PCTL公式有效性所需的模型检测算法。简要讨论PCTL模型检测的复杂性。 4. 模块4：连续时间马尔可夫链 - 描述：通过引入实时时间，增强离散时间马尔可夫链，并讨论结果模型形式随时间演变的方式。计算不同CMTC的稳定状态，并讨论如何使用均匀化方法有效计算瞬时概率。 5. 模块5：连续随机逻辑 - 描述：介绍连续随机逻辑的语法和语义，并描述如何进行不同类型CSL公式的模型检测。尤其是，模型检测时间限制直到操作符需要应用我们在前一个模块中讨论的均匀化概念。
Name:Module 1: Computational Tree Logic
Description:We introduce Labeled Transition Systems (LTS), the syntax and semantics of Computational Tree Logic (CTL) and discuss the model checking algorithms that are necessary to compute the satisfaction set for specific CTL formulas.
Name:Discrete Time Markov Chains
Description:We enhance transition systems by discrete time and add probabilities to transitions to model probabilistic choices. We discuss important properties of DTMCs, such as the memoryless property and time-homogeneity. State classification can be used to determine the existence of the limiting and / or stationary distribution.
Name:Probabilistic Computational Tree Logic
Description:We discuss the syntax and semantics of Probabilistic Computational Tree logic and check out the model checking algorithms that are necessary to decide the validity of different kinds of PCTL formulas. We shortly discuss the complexity of PCTL model checking.
Name:Continuous Time Markov Chains
Description:We enhance Discrete-Time Markov Chains with real time and discuss how the resulting modelling formalism evolves over time. We compute the steady-state for different kinds of CMTCs and discuss how the transient probabilities can be efficiently computed using a method called uniformisation.
Name:Continuous Stochastic Logic
Description:We introduce the syntax and semantics of Continuous Stochastic Logic and describe how the different kinds of CSL formulas can be model checked. Especially, model checking the time bounded until operator requires applying the concept of uniformisation, which we have discussed in the previous module.
The integration of ICT (information and communications technology) in different applications is rapidly increasing in e.g. Embedded and Cyber physical systems, Communication protocols and Transportation systems. Hence, their reliability and dependability increasingly depends on software. Defects can be fatal and extremely costly (with regards to mass-production of products and safety-critical systems). First, a model of the real system has to be built. In the simplest case, the model reflects all possible states that the system can reach and all possible transitions between states in a (labelled) State Transition System. When adding probabilities and discrete time to the model, we are dealing with so-called Discrete-time Markov chains which in turn can be extended with continuous timing to Continuous-time Markov chains. Both formalisms have been used widely for modeling and performance and dependability evaluation of computer and communication systems in a wide variety of domains. These formalisms are well understood, mathematically attractive while at the same time flexible enough to model complex systems. Model checking focuses on the qualitative evaluation of the model. As formal verification method, model checking analyzes the functionality of the system model. A property that needs to be analyzed has to be specified in a logic with consistent syntax and semantics. For every state of the model, it is then checked whether the property is valid or not. The main focus of this course is on quantitative model checking for Markov chains, for which we will discuss efficient computational algorithms. The learning objectives of this course are as follows: - Express dependability properties for different kinds of transition systems . - Compute the evolution over time for Markov chains. - Check whether single states satisfy a certain formula and compute the satisfaction set for properties.
