中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Subject: 计算机软件 ; 计算机软件::软件理论
Title:
连续时间马尔科夫链模型上的模型检测算法研究与工具实现
Author: 高杨
Issued Date: 2013-05-27
Supervisor: 詹乃军
Major: 计算机软件与理论
Degree Grantor: 中国科学院大学
Place of Degree Grantor: 北京
Degree Level: 硕士
Keyword: 模型检测 ; 连续时间马尔科夫链 ; 形式化 ; 概率模型检测工具
Abstract:     连续时间马尔科夫链(CTMC)在网络性能分析、模型检测和系统生物学等领域受到了广泛的关注。本文关注以连续时间马尔科夫链为模型、以条件连续随机逻辑(CCSL)为性质描述语言的概率模型检测问题。CCSL通过引入条件概率运算符扩展了Aziz等人提出的连续随机逻辑(CSL),从而可以表达和检测CTMC更多的性质,本文针对CCSL逻辑提出了基于参数乘积CTMC的近似模型检测算法,并分析了该算法的理论时间复杂度。进而,本文介绍了针对CSLCCSL逻辑开发的概率模型检测工具CCMC已有的概率模型检测工具如PRISMMRMC仅仅支持CSL二元Until公式,CCMC是第一个支持CSL全部语法形式和其扩展的概率模型检测工具。最后,本文通过一些实例分析展示了工具的性能和实用价值。
English Abstract:
Continuous-time Markov chains (CTMCs) have received considerable attentions in network performance analysis, model checking, and system biology. In this paper, we consider the model-checking problem of continuous-time Markov chains with respect to Conditional Continuous Stochastic Logic (CCSL). CCSL extends the logic CSL introduced by Aziz et al. with a conditional probabilistic operator, which allows us to express a richer class of properties for CTMCs.  Based on a parameterized product construction, we propose an approximate model checking algorithm with complexity analysis. After that, we present CCMC (Conditional CSL Model Checker), a model checker for CTMCs with respect to formulas specified in CCSL. Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing nested until path formulas. Moreover, CCMC supports conditional CSL formulas. Some case studies are given showing the efficiency of the tool.
Language: 英语
Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/14845
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
gymain.pdf(1331KB)----限制开放 联系获取全文

Recommended Citation:
高杨. 连续时间马尔科夫链模型上的模型检测算法研究与工具实现[D]. 北京. 中国科学院大学. 2013-05-27.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[高杨]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[高杨]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace