Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems
Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems
复制标题
DOI：
10.1007/978-3-662-45489-3
复制
发表时间：
2014-10
期刊：
影响因子：
--
通讯作者：
Anne Remke;M. Stoelinga
中科院分区：
文献类型：
--
作者：
Anne Remke;M. Stoelinga
随机模型被广泛用于各种现象的建模和分析，从心理学，语音识别到政治联盟的形成，粒子行为以及更多的应用。它们在计算机科学中的应用也很广泛，例如，在性能建模，随机算法分析和形成互联网结构的通信协议中。随机模型检验是随机分析的一个重要领域。由于其强大而系统的建模和分析随机系统的方法，它迅速流行起来。为了让年轻的研究人员了解随机模型检验的基本原理和最新技术水平，ROCKS项目组织了一个秋季学校，由荷兰NWO和德国DFG资助。学校于2012年10月22日至26日在意大利的Vahrn举行。来自该领域的主要科学家就基础和最先进的研究发表了演讲。本教程的七个章节是在岩石秋季学校开始的，总结了该领域的最新技术，围绕随机模型，抽象技术和随机模型检查三个领域。所有提交的论文都经过了至少三名程序委员会成员的两阶段审查，最终委员会决定接受所有七篇论文。随机模型检验是一个丰富的领域，它为随机系统的建模和分析提供了强大而系统的方法。存在各种各样的随机模型，这取决于所使用的概率选择（离散，连续或两者兼而有之），是否存在非确定性（马尔可夫模型与决策模型）以及模型的状态空间（离散与连续）。这些模型允许各种各样的分析方法来研究它们的行为和属性。
Stochastic models are widely used in the modeling and analysis of a wide range of phenomena, ranging from psychology, speech recognition, to political coalition forming, particle behavior, and many more applications. Their use in computer science is also wide-spread, for instance, in performance modeling, analysis of randomized algorithms, and communication protocols that form the structure of the Internet. Stochastic model checking is an important field in stochastic analysis. It has rapidly gained popularity, due to its powerful and systematic methods for modeling and analyzing stochastic systems. In order to inform young researchers about the fundamentals and state of the art in stochastic model checking, an Autumn School was organized by the ROCKS project, funded by the Dutch NWO and German DFG. The school was held during Ocotber 22-26, 2012, in Vahrn, Italy. Leading scientists from the field gave lectures on foundations as well as state-of-the-art research. The seven chapters of this tutorial were initiated at the ROCKS Autumn School, summarizing the state of the art in the field, centered around the three areas of stochastic models, abstraction techniques, and stochastic model checking. All submissions were thoroughly reviewed in a two-stage review process by at least three Program Committee members and in the end the committee decided to accept all seven papers.Stochastic model checking is a rich field, which provides powerful and systematic methods for modeling and analyzing stochastic systems. A wide variety of stochastic models exist, depending on probabilistic choices that are used (discrete, continuous, or both), on whether nondeterminism is present (Markov models versus decision models) and the state space of the models (discrete versus continuous). These models allow for a wide variety of analysis methods to investigate their behavior and properties.